Theorems · Theorem · approximation theory

ExpGrowth.expGrowthInf_mul_le

∀ {u v : ℕ → ENNReal},
  ExpGrowth.expGrowthSup u ≠ ⊥ ∨ ExpGrowth.expGrowthInf v ≠ ⊤ →
    ExpGrowth.expGrowthSup u ≠ ⊤ ∨ ExpGrowth.expGrowthInf v ≠ ⊥ →
      ExpGrowth.expGrowthInf (u * v) ≤ ExpGrowth.expGrowthSup u + ExpGrowth.expGrowthInf v

See expGrowthInf_mul_le' for a version with swapped argument u and v.

Defined in

Mathlib.Analysis.Asymptotics.ExpGrowth

Cited by

2 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound