Theorems · Theorem · real analysis
Real.posLog_mul
∀ {x y : ℝ}, (x * y).posLog ≤ x.posLog + y.posLogEstimate for log⁺ of a product. See Real.posLog_prod for a variant involving
multiple factors.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
- Real.logproof · cited by 939
- Real.log_zeroproof · cited by 84
- Real.posLogstatement · cited by 61
- Real.log_mulproof · cited by 52
- max_selfproof · cited by 43
- max_add_add_le_max_add_maxproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- ValueDistribution.proximity_mul_top_leproof · cited by 2
- Real.posLog_nat_mulproof · cited by 1
- Real.posLog_prodproof · cited by 0