Theorems · Theorem · approximation theory

ExpGrowth.expGrowthSup_mul_le

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

Defined in: Mathlib.Analysis.Asymptotics.ExpGrowth
Cited by: 1 results in Mathlib
Foundations: Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

ENNRealstatement and proof · cited by 9,879
Top.topstatement and proof · cited by 9,680
Bot.botstatement and proof · cited by 4,720
ERealstatement and proof · cited by 793
Filter.Eventually.of_forallproof · cited by 526
Nat.cast_nonneg'proof · cited by 245
ENNReal.logproof · cited by 72
Pi.add_applyproof · cited by 61
ExpGrowth.expGrowthSupstatement and proof · cited by 42
Pi.mul_applyproof · cited by 24
LE.le.trans_eq'proof · cited by 21
Filter.limsup_congrproof · cited by 20

Cited by1

Results whose statement or proof uses this declaration.

ExpGrowth.expGrowthSup_le_of_eventually_leproof · cited by 1