InterpolatedExponents.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

127 declarations, 0 contain sorry, 0 declared as axioms

Results about working with (interpolated) exponents

This files contains convenience results for working with interpolated exponents, as well as results about a particular choice of exponent that we will use for the proof of the real interpolation theorem.

Upstreaming status: mixed; some requires more design discussions

the ENNReal section is ready to go
the ComputationsInterpolatedExponents sections is also generally useful; need to find a better naming scheme for the lemmas (and address a few TODOs)
the ComputationsChoiceExponent section is specific to this particular proof of real interpolation. If we prefer a proof about Lorentz spaces, using a different approach, it may not be worth upstreaming.

Imports (1)

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Imported by 2 files

theorem ENNReal.mem_sub_Ioo the Ioc version is true for r = ∞ also line 31 source
Source comment
the Ioc version is true for r = ∞ also

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, Membership.mem, Set, Set.Ioo, OfNat.ofNat, HSub.hSub
Proof uses: Eq, LT.lt, Or, eq_zero_or_pos, False.elim, False, Eq.mp, Eq.trans, EmptyCollection.emptyCollection, congrFun', congrArg, Set.Ioo_eq_empty, of_eq_true, Not, True, not_false_eq_true, Eq.symm, And.intro, tsub_pos_of_lt, And.right and 4 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem mem_sub_Ioo {q r : ℝ≥0∞} (hr : r ≠ ⊤) (hq : q ∈ Ioo 0 r) : r - q ∈ Ioo 0 r := by
…
```
lemma ENNReal.sub_toReal_of_le line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, Eq, Real, HSub.hSub, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ENNReal.toReal_one, ENNReal.toReal_sub_of_le, ENNReal.one_ne_top, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.sub_sub_toReal_of_le line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, Eq, Real, ENNReal.toReal, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ENNReal.sub_toReal_of_le, sub_sub_cancel, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.one_sub_one_sub_eq line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, HSub.hSub
Proof uses: ENNReal.sub_sub_cancel, ENNReal.one_ne_top, LT.lt.le, And.right, LT.lt
17 instances, coercions and auxiliary constants left out.
lemma ENNReal.one_le_toReal line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, LT.lt, Top.top, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_mono, LT.lt.ne_top
17 instances, coercions and auxiliary constants left out.
lemma ENNReal.coe_rpow_ne_top line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Ne, ENNReal, HPow.hPow, ENNReal.ofReal, Top.top
Proof uses: ENNReal.rpow_ne_top_of_nonneg, ENNReal.ofReal_ne_top
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.coe_rpow_ne_top' Note this lemma can directly be applied to elements of ℝ≥0 as well line 51 source
Source comment
Note this lemma can directly be applied to elements of `ℝ≥0` as well

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Ne, ENNReal, HPow.hPow, ENNReal.ofReal, Top.top
Proof uses: ENNReal.rpow_ne_top_of_nonneg, le_of_lt, ENNReal.ofReal_ne_top
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma coe_rpow_ne_top' {a : ℝ} {q : ℝ} (hq : 0 < q) : ENNReal.ofReal a ^ q ≠ ⊤ := by finiteness
```
lemma ENNReal.coe_pow_pos line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, ENNReal, HPow.hPow, ENNReal.ofReal
Proof uses: ENNReal.rpow_pos, Iff.mpr, ENNReal.ofReal_pos, ENNReal.coe_ne_top, Real.toNNReal
16 instances, coercions and auxiliary constants left out.
lemma ENNReal.rpow_ne_top' line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, Ne, OfNat.ofNat, Top.top, HPow.hPow
Proof uses: ENNReal.rpow_ne_top_of_nonneg', lt_of_le_of_ne', zero_le
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.exp_toReal_pos' unused (one reference in an also-unused lemma) line 59 source
Source comment
unused (one reference in an also-unused lemma)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, LT.lt, Top.top, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_pos, LT.lt.ne', lt_of_lt_of_le, zero_lt_one, LT.lt.ne_top
28 instances, coercions and auxiliary constants left out.
```
lemma exp_toReal_pos' {q : ℝ≥0∞} (hq : 1 ≤ q) (hq' : q < ⊤) : 0 < q.toReal :=
…
```
lemma ENNReal.ne_top_of_Ico line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ico, Ne, Top.top
Proof uses: LT.lt.ne_top, And.right, LE.le, LT.lt
10 instances, coercions and auxiliary constants left out.
lemma ENNReal.lt_top_of_Ico line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ico, LT.lt, Top.top
Proof uses: Ne.lt_top, ENNReal.ne_top_of_Ico
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.ne_top_of_Ioo line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, Ne, Top.top
Proof uses: LT.lt.ne_top, And.right, LT.lt
9 instances, coercions and auxiliary constants left out.
lemma ENNReal.lt_top_of_Ioo line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, LT.lt, Top.top
Proof uses: Ne.lt_top, ENNReal.ne_top_of_Ioo
9 instances, coercions and auxiliary constants left out.
lemma ENNReal.toReal_mem_Ioo XXX: generalise interval bounds! line 73 source
Source comment
XXX: generalise interval bounds!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Real, ENNReal.toReal
Proof uses: And.intro, LT.lt, ENNReal.toReal_pos, LT.lt.ne', And.left, ENNReal.ne_top_of_Ioo, ENNReal.toReal_lt_of_lt_ofReal, of_eq_true, ENNReal.ofReal, Eq.trans, True, congrArg, ENNReal.ofReal_one, eq_true, And.right
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma toReal_mem_Ioo {t : ℝ≥0∞} (ht : t ∈ Ioo 0 1) : t.toReal ∈ Ioo 0 1 :=
…
```
lemma ENNReal.ofReal_mem_Ioo_0_1 XXX: generalise interval bounds! line 77 source
Source comment
XXX: generalise interval bounds!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, ENNReal, ENNReal.ofReal
Proof uses: And.intro, LT.lt, Iff.mpr, ENNReal.ofReal_pos, And.left, ENNReal.ofReal_lt_one, And.right
22 instances, coercions and auxiliary constants left out.
```
lemma ofReal_mem_Ioo_0_1 (t : ℝ) (h : t ∈ Ioo 0 1) : ENNReal.ofReal t ∈ Ioo 0 1 :=
…
```
lemma ENNReal.ne_top_of_Ioc line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioc, LT.lt, Top.top, Ne
Proof uses: LT.lt.ne_top, LE.le.trans_lt, And.right, LE.le
12 instances, coercions and auxiliary constants left out.
lemma ENNReal.pos_of_rb_Ioc line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioc, LT.lt, OfNat.ofNat
Proof uses: LT.lt.trans_le, LE.le.trans_lt, zero_le, And.left, LE.le, And.right
19 instances, coercions and auxiliary constants left out.
lemma ENNReal.ne_zero_of_Ioo line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, Ne, OfNat.ofNat
Proof uses: LT.lt.ne', pos_of_gt, And.left, LT.lt
18 instances, coercions and auxiliary constants left out.
lemma ENNReal.pos_of_Icc_1 line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Icc, OfNat.ofNat, LT.lt
Proof uses: lt_of_lt_of_le, zero_lt_one, And.left, LE.le
24 instances, coercions and auxiliary constants left out.
lemma ENNReal.pos_of_ge_1 line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, LT.lt
Proof uses: lt_of_lt_of_le, zero_lt_one
23 instances, coercions and auxiliary constants left out.
lemma ENNReal.pos_rb_of_Icc_1_inh line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Icc, OfNat.ofNat, LT.lt
Proof uses: lt_of_lt_of_le, zero_lt_one, le_trans, And.left, LE.le, And.right
24 instances, coercions and auxiliary constants left out.
lemma ENNReal.toReal_pos_of_Ioo line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, LT.lt, Real, OfNat.ofNat, ENNReal.toReal
Proof uses: ENNReal.toReal_pos, ENNReal.ne_zero_of_Ioo, LT.lt.ne_top, And.right
11 instances, coercions and auxiliary constants left out.
lemma ENNReal.toReal_ne_zero_of_Ioo line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, Ne, Real, ENNReal.toReal, OfNat.ofNat
Proof uses: Iff.mpr, And, Top.top, ENNReal.toReal_ne_zero, And.intro, ENNReal.ne_zero_of_Ioo, LT.lt.ne_top, And.right, LT.lt
14 instances, coercions and auxiliary constants left out.
lemma ENNReal.eq_of_rpow_eq TODO: check which ones are actually used line 102 source
Source comment
TODO: check which ones are actually used

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, Ne, OfNat.ofNat, Eq, HPow.hPow
Proof uses: Eq.mpr, Inv.inv, id, congrArg, Eq.symm, ENNReal.rpow_rpow_inv, congrFun
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_rpow_eq (a b : ℝ≥0∞) (c : ℝ) (hc : c ≠ 0) (h : a ^ c = b ^ c) : a = b := by
…
```
Mentions: c
lemma ENNReal.le_of_rpow_le line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, LE.le, HPow.hPow
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrArg, Eq.symm, ENNReal.rpow_rpow_inv, LT.lt.ne', Iff.mpr, ENNReal.rpow_le_rpow_iff, inv_pos_of_pos
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.coe_inv_exponent line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Eq, ENNReal.ofReal, ENNReal.toReal, Inv.inv
Proof uses: Iff.mpr, Ne, Top.top, ENNReal.ofReal_toReal_eq_iff, ENNReal.Finiteness.inv_ne_top, ne_of_gt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.preservation_positivity₀ TODO: find a better name for the next three lemmas! line 114 source
Source comment
TODO: find a better name for the next three lemmas!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Or, Ne, Top.top, LT.lt, HAdd.hAdd, HMul.hMul, HSub.hSub, Inv.inv
Proof uses: Left.add_pos_of_pos_of_nonneg, ENNReal.mul_pos, LT.lt.ne', tsub_pos_of_lt, And.right, Iff.mpr, ENNReal.inv_ne_zero, zero_le, Right.add_pos_of_nonneg_of_pos, LE.le, And.left
55 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma preservation_positivity₀ (ht : t ∈ Ioo 0 1) (hpq : p ≠ ⊤ ∨ q ≠ ⊤) :
    0 < (1 - t) * p⁻¹ + t * q⁻¹ := by
…
```
lemma ENNReal.preservation_positivity line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Ne, LT.lt, HAdd.hAdd, HMul.hMul, HSub.hSub, Inv.inv
Proof uses: ENNReal.preservation_positivity₀, Or, Eq, lt_or_gt_of_ne, Top.top, Or.inl, Ne.ne_or_ne, Or.inr, Eq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.preservation_positivity' line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Eq.symm, inv_inv, of_eq_true, Eq.trans, True, Not, False, Or, congr, And, eq_false, LT.lt.ne', and_false, not_false_eq_true, and_true, false_and, or_self
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_add_of_pos line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, Eq, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 36 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.eq_of_le_of_le line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, Eq
Proof uses: Ne, Or, eq_or_ne, LT.lt, lt_or_gt_of_ne, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, id, implies_congr, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_apply_coe TODO: should some of the following lemmas be tagged with finiteness? line 151 source
Source comment
TODO: should some of the following lemmas be tagged with finiteness?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Real, Eq, ENNReal, HPow.hPow, ite, And, OfNat.ofNat, LT.lt, Top.top
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
```
lemma rpow_apply_coe {x : ℝ≥0} {y : ℝ} :
    ENNReal.ofNNReal x ^ y = if x = 0 ∧ y < 0 then ∞ else (x ^ y : ℝ≥0) := rfl
```
lemma ENNReal.rpow_apply_coe' line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, Ne, Top.top, Eq, HPow.hPow, ite, And, OfNat.ofNat, LT.lt, NNReal, ENNReal.toNNReal
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HPow, ENNReal.coe_toNNReal, ite_congr, propext, Iff, Or, id, congrArg, ENNReal.toNNReal_eq_zero_iff, of_eq_true, Eq.trans, True, False and 5 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_lt_rpow_iff_neg line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, OfNat.ofNat, Top.top, LT.lt, Real, HPow.hPow
Proof uses: Eq.mpr, ite, And, Eq, NNReal, ENNReal.toNNReal, id, congrArg, ENNReal.rpow_apply_coe', LT.lt.ne_top, Eq.trans, congr, ite_eq_right_of_eq_false, False, congrFun', eq_false, LT.lt.ne', pos_of_gt, false_and, NNReal.rpow_lt_rpow_of_neg and 2 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.div_lt_div line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Iff, HDiv.hDiv
Proof uses: Eq.mpr, HMul.hMul, id, Eq, congrArg, propext, ENNReal.div_lt_iff, Or.inl, LT.lt.ne', ENNReal.div_mul_cancel, Iff.rfl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_lt_top_of_neg line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, LT.lt, OfNat.ofNat, HPow.hPow, Top.top
Proof uses: Iff.mp, Inv.inv, ENNReal.inv_lt_inv, Ne, LT.lt.ne', LE.le, LT.lt.le, Eq.mpr, And, Eq, id, Eq.trans, congrFun', congrArg, ENNReal.inv_top, Not, Or, congr, implies_congr, Eq.refl and 2 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_lt_top_of_pos_ne_top_ne_zero line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, Ne, OfNat.ofNat, Top.top, LT.lt, HPow.hPow
Proof uses: Or, lt_or_gt_of_ne, ENNReal.rpow_lt_top_of_neg, Ne.bot_lt, ENNReal.rpow_lt_top_of_nonneg, LT.lt.le
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_pos_of_pos_ne_top_ne_zero line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, Ne, OfNat.ofNat, Top.top, LT.lt, HPow.hPow
Proof uses: Iff.mp, Inv.inv, ENNReal.inv_lt_inv, Eq.mpr, Neg.neg, id, Eq, congrArg, Eq.symm, ENNReal.rpow_neg, ENNReal.inv_zero, ENNReal.rpow_lt_top_of_pos_ne_top_ne_zero, Iff.mpr, neg_ne_zero
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.power_estimate TODO: better name! line 190 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, HDiv.hDiv
Proof uses: Real.rpow_le_rpow_of_exponent_le, Iff.mpr, one_le_div
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma power_estimate {a b t γ : ℝ} (hγ : 0 < γ) (htγ : γ ≤ t) (hab : a ≤ b) :
    (t / γ) ^ a ≤ (t / γ) ^ b := by
…
```
lemma ENNReal.power_estimate' TODO: better name! line 196 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, HDiv.hDiv
Proof uses: lt_of_lt_of_le, Real.rpow_le_rpow_of_exponent_ge, div_pos, div_le_one_of_le₀, LT.lt.le
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma power_estimate' {a b t γ : ℝ} (ht : 0 < t) (htγ : t ≤ γ) (hab : a ≤ b) :
    (t / γ) ^ b ≤ (t / γ) ^ a := by
…
```
lemma ENNReal.rpow_le_rpow_of_exponent_le_base_le line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, ENNReal, ENNReal.ofReal, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, mul_comm, lt_of_lt_of_le, HDiv.hDiv, Real.rpow_sub, Iff.mp, Neg.neg, ENNReal.mul_le_mul_iff_right, LT.lt.ne', Iff.mpr, ENNReal.ofReal_pos, Real.rpow_pos_of_pos, ENNReal.coe_ne_top, Real.toNNReal, Eq.symm, ENNReal.ofReal_mul, le_of_lt and 24 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma ENNReal.rpow_le_rpow_of_exponent_le_base_le_enorm Note: this lemma is false if t = γ = ∞ and a < 0 ≤ b, as then t ^ a = ∞ ^ a = 0 and the statement becomes ∞ ≤ 0 * ∞ = 0 line 221 source
Source comment
Note: this lemma is false if t = γ = ∞ and a < 0 ≤ b, as then t ^ a = ∞ ^ a = 0 and the statement becomes ∞ ≤ 0 * ∞ = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, LE.le, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: Trans.trans, Eq, HAdd.hAdd, of_eq_true, Eq.trans, True, congrArg, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf', Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm and 34 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma rpow_le_rpow_of_exponent_le_base_le_enorm {a b : ℝ} {t γ : ℝ≥0∞} (ht : 0 < t) (ht' : t ≠ ∞) (htγ : t ≤ γ) (hab : a ≤ b) :
    t ^ b ≤ t ^ a * γ ^ (b - a) := by
…
```
lemma ENNReal.rpow_le_rpow_of_exponent_le_base_ge TODO: there is a lot of overlap between above proof and below line 229 source
Source comment
TODO: there is a lot of overlap between above proof and below

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, ENNReal, ENNReal.ofReal, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, mul_comm, lt_of_le_of_lt', HDiv.hDiv, Real.rpow_sub, Iff.mp, Neg.neg, ENNReal.mul_le_mul_iff_right, LT.lt.ne', Iff.mpr, ENNReal.ofReal_pos, Real.rpow_pos_of_pos, ENNReal.coe_ne_top, Real.toNNReal, Eq.symm, ENNReal.ofReal_mul, le_of_lt and 25 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma rpow_le_rpow_of_exponent_le_base_ge {a b t γ : ℝ} (hγ : 0 < γ) (htγ : γ ≤ t) (hab : a ≤ b) :
    ENNReal.ofReal (t ^ a) ≤ ENNReal.ofReal (t ^ b) * ENNReal.ofReal (γ ^ (a - b)) := by
…
```
lemma ENNReal.rpow_le_rpow_of_exponent_le_base_ge_enorm line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, LE.le, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: dite, Eq, Eq.mpr, ite, id, congr, congrArg, congrFun', Eq.trans, ite_mul, ite_congr, Eq.refl, Not, sub_zero, one_mul, MulZeroClass.zero_mul, ite_eq_left, of_eq_true, True, ENNReal.top_mul and 85 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.interp_exp_ne_top line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top
Proof uses: Iff.mp, ENNReal.inv_ne_zero, Eq.rec, LT.lt.ne', ENNReal.preservation_positivity₀, Decidable.byContradiction, Or, Not, Eq.trans, And.left, Eq.mp, And, congr, congrArg, Eq.symm, And.right
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.interp_exp_ne_top' line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Or, Ne, Top.top, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Iff.mp, ENNReal.inv_ne_zero, Eq.rec, LT.lt.ne', ENNReal.preservation_positivity₀, Eq.symm
36 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_eq line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Eq.symm, inv_inv, add_mul, LE.le, propext, tsub_add_cancel_iff_le, LT.lt.le, And.right, LT.lt, one_mul, Eq.refl
50 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.interp_exp_lt_top line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, Top.top
Proof uses: Ne.lt_top, ComputationsInterpolatedExponents.interp_exp_ne_top
37 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_lt_top' line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Or, Ne, Top.top, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt
Proof uses: Ne.lt_top, ComputationsInterpolatedExponents.interp_exp_ne_top'
38 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_between line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Ne, Top.top, LT.lt.ne, LT.lt.trans, And.right, ENNReal.one_lt_top, And.intro, Iff.mp, ENNReal.inv_lt_inv, Eq.mpr, id, congrArg, Eq.symm, add_mul, Max.max, tsub_add_eq_max, max_eq_left_of_lt, one_mul, Eq.refl, ENNReal.add_lt_add_left and 13 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.one_le_interp_exp_aux line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, LT.lt, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: LT.lt.le, LE.le.trans_lt, And.left, ComputationsInterpolatedExponents.interp_exp_between, LT.lt.trans_le, zero_lt_one
44 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.switch_exponents line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, add_comm, ENNReal.one_sub_one_sub_eq
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.one_le_interp line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, Ne, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: LT.lt, Or, lt_or_gt_of_ne, ComputationsInterpolatedExponents.one_le_interp_exp_aux, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, ComputationsInterpolatedExponents.switch_exponents
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.one_le_interp_toReal line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LE.le, OfNat.ofNat, Ne, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: ENNReal.one_le_toReal, ComputationsInterpolatedExponents.one_le_interp, Ne.lt_top, ComputationsInterpolatedExponents.interp_exp_ne_top
39 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.exp_toReal_ne_zero_of_Ico unused line 355 source
Source comment
unused

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ico, OfNat.ofNat, Ne, Real, ENNReal.toReal
Proof uses: LT.lt.ne', ENNReal.exp_toReal_pos', And.left, LE.le, LT.lt, ENNReal.lt_top_of_Ico
17 instances, coercions and auxiliary constants left out.
```
lemma exp_toReal_ne_zero_of_Ico {q p : ℝ≥0∞} (hq : q ∈ Ico 1 p) : q.toReal ≠ 0 :=
…
```
lemma ComputationsInterpolatedExponents.inv_of_interpolated_pos' line 362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt
Proof uses: Iff.mpr, Top.top, ENNReal.inv_pos, ComputationsInterpolatedExponents.interp_exp_ne_top
37 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interpolated_pos' TODO: remove, this is redundant, but for now mirror the development for reals line 367 source
Source comment
TODO: remove, this is redundant, but for now mirror the development for reals...

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: ENNReal.preservation_positivity'
36 instances, coercions and auxiliary constants left out.
```
lemma interpolated_pos' (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (ht : t ≠ ∞)
    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p :=
…
```
lemma ComputationsInterpolatedExponents.exp_toReal_pos line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_pos, LT.lt.ne'
14 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_in_Ioo_zero_top line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Or, Ne, Top.top, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: And.intro, ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, ComputationsInterpolatedExponents.interp_exp_lt_top'
38 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top line 379 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Real, ENNReal.toReal, Inv.inv
Proof uses: Eq.rec, Eq, inv_pos_of_pos, ComputationsInterpolatedExponents.exp_toReal_pos, Eq.symm, ENNReal.toReal_inv
33 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.inv_toReal_ne_zero_of_ne_top line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Real, ENNReal.toReal, Inv.inv
Proof uses: LT.lt.ne', ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top
17 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_toReal_pos line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_pos, LT.lt.ne', ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, ComputationsInterpolatedExponents.interp_exp_ne_top
38 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_toReal_pos' line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Or, Ne, Top.top, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_pos, LT.lt.ne', ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, ComputationsInterpolatedExponents.interp_exp_ne_top'
40 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_inv_pos line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: Eq.rec, inv_pos_of_pos, ComputationsInterpolatedExponents.interp_exp_toReal_pos, Eq.symm, ENNReal.toReal_inv
55 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.interp_exp_inv_ne_zero line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: LT.lt.ne', ComputationsInterpolatedExponents.interp_exp_inv_pos
39 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.preservation_interpolation line 404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ENNReal.toReal_mul, ENNReal.toReal_add, ENNReal.mul_ne_top, ENNReal.sub_ne_top, ENNReal.one_ne_top, ENNReal.Finiteness.inv_ne_top, ne_of_gt, ENNReal.ne_top_of_Ioo, Eq.refl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.preservation_positivity_inv_toReal line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Real, HAdd.hAdd, HMul.hMul, HSub.hSub, ENNReal.toReal, Inv.inv
Proof uses: Eq.mpr, id, Eq, LE.le, And.right, ENNReal.toReal_mem_Ioo, Top.top, Or, eq_or_ne, congrArg, Eq.trans, congrFun', ENNReal.inv_top, MulZeroClass.mul_zero, zero_add, mul_pos, And.left, ENNReal.toReal_inv, inv_pos_of_pos, ComputationsInterpolatedExponents.exp_toReal_pos and 8 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.ne_inv_toReal_exponents line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Real, ENNReal.toReal, Inv.inv
Proof uses: Eq, Eq.mpr, id, congrArg, Eq.symm, inv_inv, ENNReal.ofReal, Iff.mpr, Top.top, ENNReal.ofReal_toReal_eq_iff, ENNReal.inv_ne_top, LT.lt.ne'
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, ComputationsInterpolatedExponents.preservation_interpolation, Eq.symm, propext, sub_ne_zero, eq_of_heq, HEq, Eq.refl, HEq.refl, mul_sub, tsub_add_eq_tsub_tsub, LE.le, one_mul, tsub_add_cancel_iff_le, LT.lt.le, And.right, sub_mul, HSub and 12 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.ne_sub_toReal_exp line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Real, HSub.hSub, ENNReal.toReal, Inv.inv
Proof uses: sub_ne_zero_of_ne, Ne.symm, ComputationsInterpolatedExponents.ne_inv_toReal_exponents
18 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp, Eq.mpr, id, congrArg, ENNReal.toReal_inv
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp₁ line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: Ne.symm, ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, ComputationsInterpolatedExponents.switch_exponents
36 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₁ line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, GT.gt, ENNReal.ofReal, Real, abs, ENNReal.toReal
Proof uses: Iff.mpr, ENNReal.ofReal_pos, inv_pos_of_pos, abs_sub_pos, ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp₁
74 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₀ line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, GT.gt, ENNReal.ofReal, Real, abs, ENNReal.toReal
Proof uses: Iff.mpr, ENNReal.ofReal_pos, inv_pos_of_pos, abs_sub_pos, Ne.symm, ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp
74 instances, coercions and auxiliary constants left out.
lemma ComputationsInterpolatedExponents.exp_lt_iff line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Or, lt_or_gt_of_ne, Iff.intro, False.elim, not_le_of_gt, le_of_lt, And.left, ComputationsInterpolatedExponents.interp_exp_between, LT.lt.le, And.right, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, ComputationsInterpolatedExponents.switch_exponents
39 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.exp_gt_iff line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Or, lt_or_gt_of_ne, Iff.intro, And.left, ComputationsInterpolatedExponents.interp_exp_between, False.elim, not_le_of_gt, LT.lt.le, And.right, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, ComputationsInterpolatedExponents.switch_exponents
39 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.exp_lt_exp_gt_iff line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Eq.mpr, id, congrArg, propext, ComputationsInterpolatedExponents.exp_lt_iff, Eq.symm, ComputationsInterpolatedExponents.exp_gt_iff, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, ComputationsInterpolatedExponents.switch_exponents, Iff.rfl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.exp_gt_exp_lt_iff line 503 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Eq.mpr, id, congrArg, propext, ComputationsInterpolatedExponents.exp_gt_iff, Eq.symm, ComputationsInterpolatedExponents.exp_lt_iff, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, ComputationsInterpolatedExponents.switch_exponents, Iff.rfl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.exp_lt_iff₁ line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, ComputationsInterpolatedExponents.exp_gt_exp_lt_iff, ComputationsInterpolatedExponents.exp_gt_iff
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsInterpolatedExponents.exp_gt_iff₁ line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, ComputationsInterpolatedExponents.exp_lt_exp_gt_iff, ComputationsInterpolatedExponents.exp_lt_iff
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def ComputationsChoiceExponent.ζ line 540 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real
Proof uses: HDiv.hDiv, HMul.hMul, HAdd.hAdd, HSub.hSub, OfNat.ofNat, ENNReal.toReal, Inv.inv
12 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.ζ_equality₁ line 544 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HSub.hSub, Inv.inv
Proof uses: id, Ne, ENNReal.toReal_ne_zero_of_Ioo, Eq.mpr, congrArg, Eq.symm, mul_div_mul_right, mul_assoc, ENNReal.sub_toReal_of_le, LT.lt.le, And.right, LT.lt, HDiv, Eq.rec, Eq.refl, HMul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast and 41 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₂ line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HSub.hSub, Inv.inv
Proof uses: id, LT.lt, Neg.neg, Eq.mpr, congrArg, propext, neg_neg_iff_pos, sub_pos, LE.le, Eq.symm, ENNReal.toReal_one, ENNReal.toReal_strict_mono, ENNReal.one_ne_top, And.right, mul_div_mul_right, LT.lt.ne, mul_assoc, ENNReal.sub_toReal_of_le, LT.lt.le, HDiv and 46 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_symm line 570 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Eq, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HSub.hSub
Proof uses: id, Eq.mpr, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Inv.inv, Neg.neg, congrArg, Eq.symm, mul_div_mul_right, Mathlib.Meta.Positivity.nz_of_isNegNat, Mathlib.Meta.NormNum.isInt_neg, Int.ofNat, Int.negOfNat, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Int, Bool and 17 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₃ line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_equality₁, Eq.symm, ComputationsInterpolatedExponents.preservation_interpolation, ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, mul_pos, ComputationsInterpolatedExponents.interp_exp_toReal_pos, ComputationsInterpolatedExponents.exp_toReal_pos, mul_div_mul_right, LT.lt.ne', Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring and 42 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₄ line 611 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_symm, ComputationsChoiceExponent.ζ_equality₃, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, add_comm, ENNReal.sub_sub_cancel, LT.lt.le, And.right, Eq.refl
52 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₅ line 624 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ENNReal.toReal, ComputationsChoiceExponent.ζ, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_equality₃, congrFun', inv_div, div_eq_mul_inv, mul_inv, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 54 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₆ line 643 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ENNReal.toReal, ComputationsChoiceExponent.ζ, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_symm, ComputationsChoiceExponent.ζ_equality₅, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, add_comm, ENNReal.one_sub_one_sub_eq
56 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₇ line 654 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_equality₁, Eq.symm, ComputationsInterpolatedExponents.preservation_interpolation, congrFun', Eq.trans, ENNReal.inv_top, sub_zero, mul_pos, ENNReal.toReal_pos, LT.lt.ne', ComputationsInterpolatedExponents.interp_exp_toReal_pos, mul_div_mul_right, HDiv, Eq.rec, Eq.refl, Trans.trans, ENNReal.toReal_inv and 45 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_equality₈ line 687 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.ζ_symm, ComputationsChoiceExponent.ζ_equality₇, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, ENNReal.one_sub_one_sub_eq, add_comm
50 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_eq_top_top line 699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, ComputationsChoiceExponent.ζ_equality₂, Eq.symm, ComputationsInterpolatedExponents.preservation_interpolation, congrFun', congr, Eq.trans, ENNReal.inv_top, sub_zero, mul_comm, div_eq_mul_inv, mul_inv_cancel₀, LT.lt.ne', mul_pos, ComputationsInterpolatedExponents.interp_exp_inv_pos, Eq.refl
80 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_iff_aux line 712 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Iff, Real, HDiv.hDiv, HMul.hMul, ENNReal.toReal, HSub.hSub, Or, And
Proof uses: Eq.mpr, id, Eq, congrArg, propext, div_pos_iff, Neg.neg, Eq.symm, Left.neg_pos_iff, neg_mul_eq_mul_neg, mul_pos_iff_of_pos_left, ComputationsInterpolatedExponents.exp_toReal_pos, neg_sub, of_eq_true, Eq.trans, True, congrFun', congr, HAdd.hAdd, LE.le and 1 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.preservation_inequality line 726 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, LT.lt, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_lt_toReal, ComputationsInterpolatedExponents.interp_exp_ne_top
38 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.preservation_inequality' line 731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, LT.lt, Real, ENNReal.toReal
Proof uses: ENNReal.toReal_lt_toReal, ComputationsInterpolatedExponents.interp_exp_ne_top
38 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.preservation_inequality_of_lt₀ line 736 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Real, ENNReal.toReal
Proof uses: Iff.mpr, ENNReal.toReal_lt_toReal, LT.lt.ne_top, ComputationsInterpolatedExponents.interp_exp_ne_top, LT.lt.ne, ComputationsInterpolatedExponents.exp_gt_iff
39 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.preservation_inequality_of_lt₁ line 742 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Ne, Top.top, Real, ENNReal.toReal
Proof uses: Iff.mpr, ENNReal.toReal_lt_toReal, ComputationsInterpolatedExponents.interp_exp_ne_top, LT.lt.ne, ComputationsInterpolatedExponents.exp_lt_iff₁
40 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.ζ_pos_toReal_iff₀ line 749 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, ComputationsChoiceExponent.ζ_equality₃, ComputationsChoiceExponent.ζ_pos_iff_aux
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_toReal_iff₁ line 759 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, ComputationsChoiceExponent.ζ_equality₄, ComputationsChoiceExponent.ζ_pos_iff_aux
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_iff_aux₀ line 770 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And, Inv.inv
Proof uses: id, Eq.mpr, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HSub.hSub, Eq, congrArg, propext, div_pos_iff, Neg.neg, Eq.symm, Left.neg_pos_iff, neg_mul_eq_mul_neg, mul_pos_iff_of_pos_left, ComputationsInterpolatedExponents.preservation_positivity_inv_toReal, neg_sub, of_eq_true, Eq.trans, True and 4 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.inv_toReal_iff line 785 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Iff, Real, ENNReal.toReal, Inv.inv
Proof uses: Iff.trans, ENNReal.toReal_lt_toReal, LT.lt.ne, Top.top, Iff.mpr, ENNReal.inv_lt_top, ENNReal.inv_lt_inv
15 instances, coercions and auxiliary constants left out.
lemma ComputationsChoiceExponent.ζ_pos_iff line 789 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrArg, propext, ComputationsChoiceExponent.ζ_pos_iff_aux₀, ComputationsChoiceExponent.inv_toReal_iff, Iff.rfl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_iff' line 797 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, id, congrArg, propext, ComputationsChoiceExponent.ζ_pos_iff, Eq.symm, ComputationsInterpolatedExponents.exp_lt_iff, ComputationsInterpolatedExponents.exp_gt_iff, Iff.rfl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_iff_of_lt₀ line 806 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, Or, And, id, congrArg, propext, ComputationsChoiceExponent.ζ_pos_iff', LT.lt.ne, Not, not_lt_of_gt, Eq.mp, Eq.symm, ComputationsInterpolatedExponents.exp_gt_iff, Iff.intro, False.elim, Iff.mpr, Classical.or_iff_not_imp_left, And.intro
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_pos_iff_of_lt₁ line 816 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, ComputationsInterpolatedExponents.exp_gt_exp_lt_iff, ComputationsChoiceExponent.ζ_pos_iff_of_lt₀
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff_aux₀ line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And, Inv.inv
Proof uses: id, Eq.mpr, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HSub.hSub, Eq, congrArg, propext, div_neg_iff, Neg.neg, Eq.symm, Left.neg_pos_iff, neg_mul_eq_mul_neg, mul_pos_iff_of_pos_left, ComputationsInterpolatedExponents.preservation_positivity_inv_toReal, neg_sub, of_eq_true, Eq.trans, True and 4 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff line 839 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrArg, propext, ComputationsChoiceExponent.ζ_neg_iff_aux₀, ComputationsChoiceExponent.inv_toReal_iff, Iff.rfl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff' line 845 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, id, congrArg, propext, ComputationsChoiceExponent.ζ_neg_iff, Eq.symm, ComputationsInterpolatedExponents.exp_lt_iff, ComputationsInterpolatedExponents.exp_gt_iff, Iff.rfl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff_of_lt₀ line 854 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, Or, And, id, congrArg, propext, ComputationsChoiceExponent.ζ_neg_iff', LT.lt.ne, Not, not_lt_of_gt, Eq.mp, Eq.symm, ComputationsInterpolatedExponents.exp_gt_iff, Iff.intro, False.elim, Iff.mpr, Classical.or_iff_not_imp_left, And.intro, Iff.mp, Decidable.not_and_iff_not_or_not'
44 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff_of_lt₁ line 864 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, ComputationsInterpolatedExponents.exp_lt_exp_gt_iff, ComputationsChoiceExponent.ζ_neg_iff_of_lt₀
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff_aux line 872 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, LT.lt, OfNat.ofNat, Ne, Top.top, Iff, Real, HDiv.hDiv, HMul.hMul, ENNReal.toReal, HSub.hSub, Or, And
Proof uses: Eq.mpr, id, Eq, congrArg, propext, div_neg_iff, Neg.neg, Eq.symm, Left.neg_pos_iff, neg_mul_eq_mul_neg, mul_pos_iff_of_pos_left, ComputationsInterpolatedExponents.exp_toReal_pos, neg_sub, of_eq_true, Eq.trans, True, congrFun', congr, HAdd.hAdd, LE.le and 1 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_toReal_iff₀ line 886 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, ComputationsChoiceExponent.ζ_equality₃, ComputationsChoiceExponent.ζ_neg_iff_aux
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_toReal_iff₁ line 897 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, ComputationsChoiceExponent.ζ_equality₄, ComputationsChoiceExponent.ζ_neg_iff_aux
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_neg_iff₀ line 908 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Iff, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal, Or, And
Proof uses: Eq.mpr, id, congrArg, propext, ComputationsChoiceExponent.ζ_neg_toReal_iff₀, ComputationsChoiceExponent.preservation_inequality, ComputationsChoiceExponent.preservation_inequality', Iff.rfl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_ne_zero line 918 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: div_ne_zero, HMul.hMul, HAdd.hAdd, HSub.hSub, Inv.inv, mul_ne_zero, LT.lt.ne', ComputationsInterpolatedExponents.preservation_positivity_inv_toReal, sub_ne_zero_of_ne, Ne.symm, Eq, Eq.mpr, id, congrArg, Eq.symm, inv_inv, ENNReal.ofReal, ENNReal.coe_inv_exponent
42 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀ line 931 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, LE.le, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Iff.intro, Or, Decidable.lt_or_eq_of_le, Iff.mp, ComputationsChoiceExponent.ζ_neg_iff_of_lt₀, False.elim, ComputationsChoiceExponent.ζ_ne_zero, LT.lt.ne, LT.lt.le, Iff.mpr
45 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₁ line 942 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Iff, LE.le, Real, ComputationsChoiceExponent.ζ, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, ComputationsInterpolatedExponents.exp_lt_exp_gt_iff, ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.one_sub_ioo_toReal line 950 source
lemma ComputationsChoiceExponent.eq_exponents₀ line 957 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ENNReal.toReal, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, mul_comm_div, Eq.symm, mul_div_assoc, add_div', ComputationsInterpolatedExponents.ne_sub_toReal_exp, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 53 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₂ line 984 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal
Proof uses: Eq.mpr, id, congrArg, div_eq_inv_mul, mul_div_assoc, mul_assoc, ENNReal.toReal_inv, Eq.symm, mul_add, mul_comm_div, add_div', ComputationsInterpolatedExponents.ne_sub_toReal_exp, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring and 56 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₁ line 1012 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal, Neg.neg
Proof uses: Eq.mpr, id, congrArg, mul_comm_div, Eq.symm, mul_div_assoc, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.Common.sub_congr and 42 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₃ TODO: simplify these proofs with statements above line 1033 source
Source comment
TODO: simplify these proofs with statements above

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal, Neg.neg
Proof uses: Eq.mpr, id, congrArg, mul_comm_div, Eq.symm, mul_div_assoc, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul and 42 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma eq_exponents₃ (ht : t ∈ Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁)
    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :
    (p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal)) * (q.toReal - q₀.toReal) =
      - t.toReal * p₁⁻¹.toReal * q.toReal := by
…
```
lemma ComputationsChoiceExponent.eq_exponents₄ line 1055 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, Real, HDiv.hDiv, ENNReal.toReal, Inv.inv, HSub.hSub, Neg.neg
Proof uses: Trans.trans, HMul.hMul, Eq.mpr, id, congrArg, div_eq_mul_inv, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 34 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₅ line 1061 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, ENNReal.toReal, Neg.neg, HDiv.hDiv
Proof uses: Eq.mpr, id, congrArg, ComputationsChoiceExponent.eq_exponents₄, neg_mul, neg_neg, ComputationsChoiceExponent.eq_exponents₀, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, ComputationsInterpolatedExponents.switch_exponents, ENNReal.one_sub_one_sub_eq, Eq.refl
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₆ line 1068 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal
Proof uses: Eq.mpr, Neg.neg, id, congrArg, Eq.symm, neg_neg, ComputationsChoiceExponent.eq_exponents₄, neg_mul, ComputationsChoiceExponent.eq_exponents₁, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, Ne.symm, ComputationsInterpolatedExponents.switch_exponents, Eq.refl
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₇ line 1075 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal, Neg.neg
Proof uses: Eq.mpr, id, congrArg, div_eq_mul_inv, ENNReal.toReal_inv, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 40 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ComputationsChoiceExponent.eq_exponents₈ line 1088 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, Top.top, Real, HDiv.hDiv, ENNReal.toReal
Proof uses: Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 26 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.