OAI/Analysis/ProductSpaces/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IndependentProducts.exponentialLaw_hypotheses line 12
2. lemma OAI.IndependentProducts.exponential_midpoint_parameter line 28
3. theorem OAI.IndependentProducts.main_exponential line 54

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, HMul.hMul, HDiv.hDiv, Nat, OAI.IndependentProducts.excessConstant, OAI.IndependentProducts.averagedMidpointModulus, Subtype, MeasureTheory.AEEqFun, OAI.IndependentProducts.Sample, OAI.IndependentProducts.Edge, OAI.IndependentProducts.productMeasure, OAI.IndependentProducts.exponentialLaw, Membership.mem, AddSubgroup, MeasureTheory.Lp, ENNReal and 3 more

   Proof uses: And.intro, HSub.hSub, OAI.IndependentProducts.exponential_midpoint_parameter, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mpr, eq_of_heq, LE, Eq, HEq, HEq.refl, Eq.symm, inferInstance, CommGroupWithZero, id and 79 more

   221 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/IndependentProducts.lean:95 (same statement text; different proof or body). Qualify references as OAI.IndependentProducts.main_exponential@path.

   Tactic trace: 10 steps

   Open to load the checked before-and-after goal states.