Carleson/ToMathlib/Data/ENNReal.lean

GitHub source file

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

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

14 declarations, 0 contain sorry, 0 declared as axioms

ENNReal manipulation lemmas

Imports (3)
Imported by 2 files
  1. theorem ENNReal.coe_lt_iff_lt_toNNReal line 24 source

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

    Statement uses: ENNReal, NNReal, Ne, Top.top, Iff, LT.lt, ENNReal.toNNReal

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, ENNReal.toNNReal_coe, propext, ENNReal.toNNReal_lt_toNNReal, ENNReal.coe_ne_top, of_eq_true, iff_self

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem ENNReal.le_mul_top_self line 29 source

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

    Statement uses: ENNReal, LE.le, HMul.hMul, Top.top

    Proof uses: Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Eq.symm, one_mul, mul_le_mul', OrderTop.le_top, le_refl

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma ENNReal.coe_biSup line 34 source

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

    Statement uses: Set, NNReal, BddAbove, Set.range, Eq, ENNReal, iSup, Membership.mem

    Proof uses: Eq.mpr, id, congrArg, ENNReal.coe_iSup, Exists, LE.le, funext, forall_congr, implies_congr, Eq.refl, Eq.mp, Exists.intro, ciSup_le', SupSet, Eq.rec, Bornology.IsBounded.bddAbove, Bornology.IsBounded, Real, OfNat.ofNat, Eq.trans and 5 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  4. lemma ENNReal.biSup_add_biSup unused line 49 source

    Source comment

    unused

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

    Statement uses: Set, ENNReal, Membership.mem, Exists, And, LE.le, HAdd.hAdd, Eq, iSup

    Proof uses: EmptyCollection.emptyCollection, Set.Nonempty, Or, Set.eq_empty_or_nonempty, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, funext, Bot.bot, False, iSup_congr_Prop, Iff.of_eq, congrFun', Eq.refl, iSup_neg, Not, not_false_eq_true and 12 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    lemma biSup_add_biSup {f g : ι → ℝ≥0∞} (h : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, f i + g j ≤ f k + g k) :
    (⨆ i ∈ s, f i) + ⨆ i ∈ s, g i = ⨆ i ∈ s, f i + g i := by
…

    Mentions: g, s, k

  5. lemma ENNReal.finsetSum_biSup unused line 59 source

    Source comment

    unused

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

    Statement uses: Set, Finset, ENNReal, Membership.mem, Exists, And, LE.le, Eq, Finset.sum, iSup

    Proof uses: Finset.cons_induction, of_eq_true, OfNat.ofNat, EmptyCollection.emptyCollection, Eq.trans, True, congrArg, funext, ENNReal.iSup_zero, eq_self, Not, Eq.mpr, Finset.cons, HAdd.hAdd, id, congr, Finset.sum_cons, iSup_congr_Prop, Iff.of_eq, Eq.refl and 8 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma finsetSum_biSup {f : α → ι → ℝ≥0∞}
    (hf : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :
    ∑ a ∈ t, ⨆ i ∈ s, f a i = ⨆ i ∈ s, ∑ a ∈ t, f a i := by
…

    Mentions: s, k

  6. lemma ENNReal.biSup_add_le_add_biSup line 69 source

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

    Statement uses: Set, ENNReal, LE.le, iSup, Membership.mem, HAdd.hAdd

    Proof uses: iSup₂_le, add_le_add, le_biSup

    31 instances, coercions and auxiliary constants left out.

  7. lemma ENNReal.biSup_finsetSum_le_finsetSum_biSup line 73 source

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

    Statement uses: Set, Finset, ENNReal, LE.le, iSup, Membership.mem, Finset.sum

    Proof uses: Finset.cons_induction, of_eq_true, EmptyCollection.emptyCollection, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, funext, ENNReal.iSup_zero, Not, Eq.mpr, Finset.cons, HAdd.hAdd, id, Eq, congr, iSup_congr_Prop, Iff.of_eq, Eq.refl and 4 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  8. lemma ENNReal.edist_sum_le_sum_edist line 83 source

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

    Statement uses: Finset, SeminormedAddCommGroup, LE.le, ENNReal, EDist.edist, Finset.sum

    Proof uses: Finset.cons_induction, of_eq_true, EmptyCollection.emptyCollection, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, WeakPseudoEMetricSpace.edist_self, Not, Membership.mem, Eq.mpr, Finset.cons, HAdd.hAdd, id, Eq, congr, Finset.sum_cons, LE.le.trans, edist_add_add_le and 1 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  9. lemma ENNReal.enorm_sum_eq_sum_enorm line 91 source

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

    Statement uses: Finset, Real, Membership.mem, LE.le, OfNat.ofNat, Eq, ENNReal, ENorm.enorm, Finset.sum

    Proof uses: Finset.cons_induction, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, enorm_zero, eq_self, Not, Finset.cons, Eq.mpr, HAdd.hAdd, id, congr, Finset.sum_cons, And.left, Eq.mp, And, Or and 10 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  10. lemma ENNReal.enorm_enorm_sub_enorm_le The reverse triangle inequality for enorm line 105 source

    Source documentation

    The reverse triangle inequality for enorm.

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

    Statement uses: NormedAddCommGroup, LE.le, ENNReal, ENorm.enorm, HSub.hSub

    Proof uses: Eq.mpr, id, Eq, congrArg, enorm_eq_self, HAdd.hAdd, propext, tsub_le_iff_right, Eq.symm, sub_add_cancel, enorm_add_le

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    lemma enorm_enorm_sub_enorm_le {E} [NormedAddCommGroup E] {x y : E} : ‖‖x‖ₑ - ‖y‖ₑ‖ₑ ≤ ‖x - y‖ₑ := by
…

    Mentions: E

  11. lemma ENNReal.exists_biSup_le_enorm_add_eps line 110 source

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

    Statement uses: Set, SeminormedAddCommGroup, NNReal, LT.lt, OfNat.ofNat, Set.Nonempty, Bornology.IsBounded, Set.image, Exists, And, Membership.mem, LE.le, ENNReal, iSup, ENorm.enorm, HAdd.hAdd

    Proof uses: Classical.byContradiction, Not, Eq.mpr, id, Eq, Eq.trans, forall_congr, LT.lt.le, Eq.mp, binderNameHint, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Ne, Top.top, congrArg, ne_eq, propext, iSup₂_eq_top, Mathlib.Tactic.Push.not_forall_eq and 22 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  12. lemma ENNReal.exists_enorm_sub_eps_le_biInf line 126 source

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

    Statement uses: Set, SeminormedAddCommGroup, NNReal, LT.lt, OfNat.ofNat, Set.Nonempty, Exists, And, Membership.mem, LE.le, ENNReal, HSub.hSub, ENorm.enorm, iInf

    Proof uses: Eq.mpr, id, Eq, congrArg, rfl, IsGLB, Set.image, isGLB_biInf, Classical.byContradiction, Not, lowerBounds, HAdd.hAdd, Eq.mp, propext, Set.mem_image, LT.lt.le, Iff.mp, lt_tsub_iff_right, Eq.trans, binderNameHint and 59 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  13. lemma ENNReal.biInf_enorm_sub_le line 143 source

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

    Statement uses: Set, SeminormedAddCommGroup, LE.le, ENNReal, iInf, Membership.mem, ENorm.enorm, HSub.hSub, HAdd.hAdd, iSup

    Proof uses: Eq, EmptyCollection.emptyCollection, Set.Nonempty, Or, Set.eq_empty_or_nonempty, of_eq_true, Eq.trans, Top.top, True, congr, congrArg, funext, False, iInf_congr_Prop, Iff.of_eq, Eq.refl, iInf_neg, Not, not_false_eq_true, iInf_top and 24 more

    100 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  14. lemma Real.enorm_le_enorm Transfer an inequality over ℝ to one of ENorms over ℝ≥0∞ line 159 source

    Source documentation

    Transfer an inequality over ℝ to one of ENorms over ℝ≥0∞.

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

    Statement uses: Real, LE.le, OfNat.ofNat, ENNReal, ENorm.enorm

    Proof uses: Eq.mpr, ENNReal.ofReal, id, Eq, congrArg, Real.enorm_of_nonneg, LE.le.trans, ENNReal.ofReal_le_ofReal

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    lemma Real.enorm_le_enorm {x y : ℝ} (hx : 0 ≤ x) (hy : x ≤ y) : ‖x‖ₑ ≤ ‖y‖ₑ := by
…