Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.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

16 declarations, 0 contain sorry, 0 declared as axioms

Triangle inequality for Lorentz-seminorm

In this file we prove several versions of the triangle inequality for the Lorentz seminorm, as well as simple corollaries.

Imports (4)
Imported by 3 files
  1. theorem MeasureTheory.eLorentzNorm_add_le'' line 32 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, LE.le, MeasureTheory.eLorentzNorm, HAdd.hAdd, HMul.hMul, HPow.hPow, Real, OfNat.ofNat, Nat, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst

    Proof uses: id, dite, ite, Eq, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLorentzNorm', Eq.mpr, congr, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, add_zero, MulZeroClass.mul_zero, Not, ite_eq_right, Membership.mem, Set and 104 more

    200 instances, coercions and auxiliary constants left out.

    Tactic trace: 67 steps

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

  2. def MeasureTheory.lorentz_helper The function k in the proof of Theorem 6.7 in https://doi.org/10.1007/978-3-319-30034-4 line 92 source

    Source documentation

    The function k in the proof of Theorem 6.7 in https://doi.org/10.1007/978-3-319-30034-4

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, NNReal

    Proof uses: HSMul.hSMul, HPow.hPow, Real, MeasureTheory.eLorentzNorm', HSub.hSub, OfNat.ofNat, ENNReal.toReal, HMul.hMul, Inv.inv, MeasureTheory.rearrangement

    18 instances, coercions and auxiliary constants left out.

    noncomputable def lorentz_helper (f : α → ε) (p q : ℝ≥0∞) (μ : Measure α) : ℝ≥0 → ℝ≥0∞ :=
…
  3. lemma MeasureTheory.eLpNorm_lorentz_helper line 96 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, Ne, OfNat.ofNat, Top.top, LE.le, MeasureTheory.eLorentzNorm', Eq, MeasureTheory.eLpNorm, NNReal, MeasureTheory.lorentz_helper, ENNReal.conjExponent, MeasureTheory.MeasureSpace.volume

    Proof uses: id, Aesop.BuiltinRules.not_intro, Not, False, False.elim, Eq.mp, Eq.trans, Eq.symm, ENNReal.HolderConjugate.ne_zero, ENNReal.HolderConjugate.conjExponent, dite, Eq.mpr, HSMul.hSMul, HPow.hPow, Real, HSub.hSub, ENNReal.toReal, HMul.hMul, Inv.inv, MeasureTheory.rearrangement and 76 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 53 steps

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

  4. theorem MeasureTheory.antitone_rpow_inv_sub_inv line 148 source

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

    Statement uses: ENNReal, LE.le, Ne, OfNat.ofNat, Antitone, NNReal, HPow.hPow, Real, HSub.hSub, Inv.inv, ENNReal.toReal

    Proof uses: id, Aesop.BuiltinRules.not_intro, Eq, False, False.elim, Eq.mp, Eq.trans, eq_false, Not, Eq.symm, ENNReal.rpow_le_rpow_of_nonpos, Eq.mpr, HAdd.hAdd, congrArg, zero_add, dite, Top.top, of_eq_true, True, congrFun' and 5 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  5. lemma MeasureTheory.antitone_lorentz_helper line 166 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, LE.le, OfNat.ofNat, Ne, Top.top, Antitone, NNReal, MeasureTheory.lorentz_helper

    Proof uses: id, Eq.mpr, HSMul.hSMul, HPow.hPow, Real, MeasureTheory.eLorentzNorm', HSub.hSub, ENNReal.toReal, HMul.hMul, Inv.inv, MeasureTheory.rearrangement, Eq, congr, congrArg, congrFun', funext, ENNReal.toReal_inv, mul_le_mul', le_refl, ENNReal.rpow_le_rpow and 8 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  6. lemma MeasureTheory.lorentz_helper_measurable line 179 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, Measurable, NNReal, MeasureTheory.lorentz_helper

    Proof uses: id, Measurable.smul, HPow.hPow, Real, MeasureTheory.eLorentzNorm', HSub.hSub, OfNat.ofNat, ENNReal.toReal, HMul.hMul, Inv.inv, MeasureTheory.rearrangement, measurable_const, Measurable.pow_const, Measurable.fun_mul, Measurable.coe_nnreal_ennreal, measurable_id', MeasureTheory.rearrangement_measurable

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  7. lemma MeasureTheory.eLorentzNorm'_eq_lintegral_lorentz_helper_mul line 183 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, Ne, OfNat.ofNat, Top.top, LE.le, MeasureTheory.eLorentzNorm', Eq, MeasureTheory.eLpNorm, NNReal, HMul.hMul, MeasureTheory.lorentz_helper, HPow.hPow, Real, HSub.hSub, ENNReal.toReal, Inv.inv and 2 more

    Proof uses: id, Eq.mpr, HSMul.hSMul, congrArg, congrFun', autoParam, Algebra.smul_mul_assoc, MeasureTheory.eLpNorm_const_smul''', Measurable.aestronglyMeasurable, Measurable.mul, Measurable.pow_const, Measurable.fun_mul, Measurable.coe_nnreal_ennreal, measurable_id', MeasureTheory.rearrangement_measurable, Pi.mul_def, Eq.rec, Eq.refl, HMul, ENorm and 32 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  8. theorem MeasureTheory.eLorentzNorm_add_le line 225 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ContinuousAdd, LE.le, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLorentzNorm, HAdd.hAdd

    Proof uses: id, dite, ite, Eq, Top.top, MeasureTheory.eLpNormEssSup, HMul.hMul, MeasureTheory.eLorentzNorm', Eq.mpr, congr, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, add_zero, Not, ite_eq_right, MeasureTheory.eLpNormEssSup_add_le, Eq.symm and 123 more

    166 instances, coercions and auxiliary constants left out.

    Tactic trace: 64 steps

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

  9. def MeasureTheory.LorentzAddConst A constant for the inequality ‖f + g‖_{L^{p,q}} ≤ C * (‖f‖_{L^{p,q}} + ‖g‖_{L^{p,q}}) line 288 source

    Source documentation

    A constant for the inequality ‖f + g‖_{L^{p,q}} ≤ C * (‖f‖_{L^{p,q}} + ‖g‖_{L^{p,q}}). It is equal to 1 if p = 0 or 1 ≤ r ≤ p and 2^(1/p) * LpAddConst r else.

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

    Statement uses: ENNReal

    Proof uses: ite, Or, Eq, OfNat.ofNat, Membership.mem, Set, Set.Icc, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst

    25 instances, coercions and auxiliary constants left out.

    noncomputable def LorentzAddConst (p r : ℝ≥0∞) : ℝ≥0∞ :=
…
  10. theorem MeasureTheory.LorentzAddConst_of_one_le line 291 source

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

    Statement uses: ENNReal, Membership.mem, Set, Set.Icc, OfNat.ofNat, Eq, MeasureTheory.LorentzAddConst

    Proof uses: Eq.mpr, ite, Or, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst, id, congrArg, MeasureTheory.LorentzAddConst.eq_1, ite_eq_left, 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.

  11. theorem MeasureTheory.LorentzAddConst_zero line 296 source

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

    Statement uses: ENNReal, Eq, MeasureTheory.LorentzAddConst, OfNat.ofNat

    Proof uses: Eq.mpr, ite, Or, Membership.mem, Set, Set.Icc, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst, id, congrArg, MeasureTheory.LorentzAddConst.eq_1, ite_eq_left, Or.inl, Eq.refl

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  12. theorem MeasureTheory.LorentzAddConst_lt_top line 301 source

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

    Statement uses: ENNReal, LT.lt, MeasureTheory.LorentzAddConst, Top.top

    Proof uses: Eq.mpr, ite, Or, Eq, OfNat.ofNat, Membership.mem, Set, Set.Icc, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst, id, congrArg, MeasureTheory.LorentzAddConst.eq_1, dite, congrFun', ite_eq_left and 16 more

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  13. lemma MeasureTheory.eLorentzNorm_add_le' line 308 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ContinuousAdd, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLorentzNorm, HAdd.hAdd, HMul.hMul, MeasureTheory.LorentzAddConst

    Proof uses: id, dite, ite, Or, Eq, OfNat.ofNat, Membership.mem, Set, Set.Icc, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENNReal.LpAddConst, Eq.mpr, congrArg, congrFun', ite_eq_left, of_eq_true, Eq.trans and 12 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  14. lemma MeasureTheory.eLorentzNorm_add_lt_top line 319 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ContinuousAdd, MeasureTheory.MemLorentz, LT.lt, MeasureTheory.eLorentzNorm, HAdd.hAdd, Top.top

    Proof uses: Trans.trans, LE.le, HMul.hMul, MeasureTheory.LorentzAddConst, MeasureTheory.eLorentzNorm_add_le', And.left, MeasureTheory.AEStronglyMeasurable, ENNReal.mul_lt_top, MeasureTheory.LorentzAddConst_lt_top, Iff.mpr, And, ENNReal.add_lt_top, And.intro, And.right

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  15. lemma MeasureTheory.MemLorentz.add line 329 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ContinuousAdd, MeasureTheory.MemLorentz, HAdd.hAdd

    Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLorentzNorm, Top.top, MeasureTheory.AEStronglyMeasurable.add, And.left, MeasureTheory.eLorentzNorm_add_lt_top

    18 instances, coercions and auxiliary constants left out.

  16. theorem MeasureTheory.eLorentzNorm_add_le_of_disjoint_support line 335 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.Measure, Disjoint, Set, Function.support, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLorentzNorm, HAdd.hAdd, HMul.hMul, ENNReal.LpAddConst

    Proof uses: id, MeasureTheory.eLpNormEssSup, LE.le.trans, MeasureTheory.eLpNormEssSup_add_le, Eq.mpr, OfNat.ofNat, Eq, congrArg, Eq.symm, one_mul, mul_le_mul', MeasureTheory.one_le_LpAddConst, le_refl, dite, ite, Top.top, MeasureTheory.eLorentzNorm', congr, ite_eq_left, of_eq_true and 43 more

    112 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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