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

20 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 3 files
  1. theorem MeasureTheory.SimpleFunc.measurable_comp TODO: tag this as @[fun_prop] (currently this gives an error) line 26 source

    Source comment

    TODO: tag this as @[fun_prop] (currently this gives an error)

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

    Statement uses: MeasurableSpace, MeasureTheory.SimpleFunc, Measurable, Function.comp

    Proof uses: MeasureTheory.SimpleFunc.measurable_bind, measurable_const

    2 instances, coercions and auxiliary constants left out.

    theorem measurable_comp [MeasurableSpace α] [MeasurableSpace γ] {f : SimpleFunc α β}
  {g : β → γ} :
    Measurable (g ∘ f) :=
…

    Mentions: g

  2. theorem MeasureTheory.SimpleFunc.measurable_comp' line 31 source

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

    Statement uses: MeasurableSpace, MeasureTheory.SimpleFunc, Measurable

    Proof uses: MeasureTheory.SimpleFunc.measurable_bind, measurable_const

    2 instances, coercions and auxiliary constants left out.

  3. theorem MeasureTheory.SimpleFunc.induction₀ Proof stolen from the mathlib SimpleFunc.induction with a minor modification that is even suggested there line 40 source

    Source comment

    Proof stolen from the mathlib `SimpleFunc.induction` with a minor modification that is even suggested there. TODO: update notation in mathlib version to match this one

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

    Statement uses: MeasurableSpace, AddZeroClass, MeasureTheory.SimpleFunc, Set, MeasurableSet, MeasureTheory.SimpleFunc.restrict, MeasureTheory.SimpleFunc.const, Disjoint, Function.support, HAdd.hAdd

    Proof uses: Finset.induction, Finset, Eq, SDiff.sdiff, Set.range, Singleton.singleton, OfNat.ofNat, Classical.propDecidable, EmptyCollection.emptyCollection, Eq.mpr, Set.univ, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.SimpleFunc.ext, of_eq_true, Eq.trans, True and 68 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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

    protected theorem induction₀ [MeasurableSpace α] [AddZeroClass γ]
    {motive : SimpleFunc α γ → Prop}
    (const : ∀ (c) {s} (_ : MeasurableSet s),
      motive ((SimpleFunc.const _ c).restrict s))
    (add : ∀ ⦃f : SimpleFunc α γ⦄ (c : γ) ⦃s : Set α⦄ (_ : MeasurableSet s), Disjoint (Function.support ⇑f) s →
      motive f → motive ((SimpleFunc.const α c).restrict s) →
        motive (f + ((SimpleFunc.const α c).restrict s)))
    (f : SimpleFunc α γ) : motive f := by
…

    Mentions: c, s

  4. lemma MeasureTheory.SimpleFunc.helper line 82 source
  5. lemma MeasureTheory.SimpleFunc.Antitone.support_eq line 218 source

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

    Statement uses: ConditionallyCompleteLinearOrderBot, AddMonoid, LinearOrder, CanonicallyOrderedAdd, OrderBot, Antitone, Eq, Set, Function.support, ite, BddAbove, Classical.propDecidable, Membership.mem, SupSet.sSup, Set.Iic, Set.Iio, Set.univ

    Proof uses: Set.ext, Eq.mpr, Iff, Not, OfNat.ofNat, id, congr, congrArg, congrFun', ite_congr, Eq.refl, Eq.trans, ite_not, dite, ite_eq_left, Mathlib.Tactic.Contrapose.contrapose_iff₂, LE.le, LT.lt, Iff.intro, csSup_le' and 27 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 58 steps

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

  6. theorem MeasureTheory.SimpleFunc.antitone_induction line 277 source

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

    Statement uses: MeasurableSpace, ConditionallyCompleteLinearOrderBot, LinearOrder, AddCommMonoid, CanonicallyOrderedAdd, OrderBot, Sub, OrderedSub, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.restrict, MeasureTheory.SimpleFunc.const, Set.Iio, Set.Iic, Set, MeasurableSet, LE.le, Function.support, HAdd.hAdd, Antitone

    Proof uses: Nat.recAux, Nat, Eq, Finset.card, SDiff.sdiff, Finset, MeasureTheory.SimpleFunc.range, Singleton.singleton, OfNat.ofNat, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.SimpleFunc.ext, of_eq_true, Eq.trans, True, congrFun' and 63 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 78 steps

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

  7. theorem MeasureTheory.SimpleFunc.induction'' line 361 source

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

    Statement uses: MeasurableSpace, LinearOrder, AddCommMonoid, CanonicallyOrderedAdd, OrderBot, Sub, OrderedSub, MeasureTheory.SimpleFunc, Set, MeasurableSet, MeasureTheory.SimpleFunc.restrict, MeasureTheory.SimpleFunc.const, LE.le, Function.support, HAdd.hAdd

    Proof uses: Nat.recAux, Nat, Eq, Finset.card, SDiff.sdiff, Finset, MeasureTheory.SimpleFunc.range, Singleton.singleton, OfNat.ofNat, Eq.mpr, Set.univ, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.SimpleFunc.ext, of_eq_true, Eq.trans, True and 45 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

  8. theorem MeasureTheory.SimpleFunc.approx_le line 420 source

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

    Statement uses: MeasurableSpace, ConditionallyCompleteLinearOrderBot, Zero, TopologicalSpace, OrderClosedTopology, OpensMeasurableSpace, Nat, Measurable, Eq, OfNat.ofNat, Bot.bot, LE.le, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.approx

    Proof uses: Eq.mpr, Finset.sup, Finset.range, ite, Classical.propDecidable, id, congrArg, MeasureTheory.SimpleFunc.approx_apply, LT.lt, Eq.trans, Membership.mem, Finset, forall_congr, implies_congr, Eq.refl, dite, congrFun', ite_eq_left, Not, ite_eq_right and 1 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  9. theorem MeasureTheory.SimpleFunc.iSup_approx_apply' Version of iSup_approx_apply for ConditionallyCompleteLinearOrderBot line 434 source

    Source comment

    Version of `iSup_approx_apply` for `ConditionallyCompleteLinearOrderBot`.

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

    Statement uses: MeasurableSpace, ConditionallyCompleteLinearOrderBot, TopologicalSpace, OrderClosedTopology, Zero, OpensMeasurableSpace, Nat, Measurable, Eq, OfNat.ofNat, Bot.bot, iSup, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.approx, LE.le

    Proof uses: le_antisymm, ciSup_le', Eq.mpr, Finset.sup, Finset.range, ite, Classical.propDecidable, id, congrArg, MeasureTheory.SimpleFunc.approx_apply, Finset.sup_le, Membership.mem, Finset, dite, congrFun', ite_eq_left, propext, le_ciSup_iff', Exists.intro, Set and 35 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

    theorem iSup_approx_apply' [ConditionallyCompleteLinearOrderBot β] [TopologicalSpace β] [OrderClosedTopology β] [Zero β]
    [MeasurableSpace β] [OpensMeasurableSpace β] (i : ℕ → β) (f : α → β) (a : α) (hf : Measurable f)
    (h_zero : (0 : β) = ⊥) : ⨆ n, (approx i f n : SimpleFunc α β) a = ⨆ (k) (_ : i k ≤ f a), i k := by
…

    Mentions: k

  10. def MeasureTheory.SimpleFunc.nnrealRatEmbed A sequence of ℝ≥0s such that its range is the set of non-negative rational numbers line 471 source

    Source documentation

    A sequence of ℝ≥0s such that its range is the set of non-negative rational numbers.

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

    Statement uses: Nat, NNReal

    Proof uses: Real.toNNReal, Real, Option.getD, Rat, Encodable.decode, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    def nnrealRatEmbed (n : ℕ) : ℝ≥0 :=
…
  11. theorem MeasureTheory.SimpleFunc.nnrealRatEmbed_encode line 474 source

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

    Statement uses: Rat, Eq, NNReal, MeasureTheory.SimpleFunc.nnrealRatEmbed, Encodable.encode, Real.toNNReal, Real

    Proof uses: Eq.mpr, Option.getD, Encodable.decode, OfNat.ofNat, id, congrArg, MeasureTheory.SimpleFunc.nnrealRatEmbed.eq_1, Option.some, Option, Encodable.encodek, Eq.refl

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  12. def MeasureTheory.SimpleFunc.nnapprox Approximate a function α → ℝ≥0 by a sequence of simple functions line 479 source

    Source documentation

    Approximate a function α → ℝ≥0 by a sequence of simple functions.

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

    Statement uses: MeasurableSpace, NNReal, Nat, MeasureTheory.SimpleFunc

    Proof uses: MeasureTheory.SimpleFunc.approx, MeasureTheory.SimpleFunc.nnrealRatEmbed

    3 instances, coercions and auxiliary constants left out.

    def nnapprox : (α → ℝ≥0) → ℕ → SimpleFunc α ℝ≥0 :=
…
  13. lemma MeasureTheory.SimpleFunc.nnapprox_le line 482 source

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

    Statement uses: MeasurableSpace, NNReal, Measurable, Nat, LE.le, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.nnapprox

    Proof uses: MeasureTheory.SimpleFunc.approx_le, MeasureTheory.SimpleFunc.nnrealRatEmbed, rfl, OfNat.ofNat

    16 instances, coercions and auxiliary constants left out.

  14. theorem MeasureTheory.SimpleFunc.monotone_nnapprox line 486 source

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

    Statement uses: MeasurableSpace, NNReal, Monotone, Nat, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.nnapprox

    Proof uses: MeasureTheory.SimpleFunc.monotone_approx, MeasureTheory.SimpleFunc.nnrealRatEmbed

    7 instances, coercions and auxiliary constants left out.

  15. lemma MeasureTheory.SimpleFunc.iSup_nnapprox_apply line 490 source

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

    Statement uses: MeasurableSpace, NNReal, Measurable, Eq, iSup, Nat, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.nnapprox

    Proof uses: le_antisymm, ciSup_le, MeasureTheory.SimpleFunc.nnapprox_le, le_of_not_gt, LT.lt, Rat, And, LE.le, OfNat.ofNat, Real.toNNReal, Real, Exists, False, Iff.mp, NNReal.lt_iff_exists_rat_btwn, MeasureTheory.SimpleFunc.nnrealRatEmbed, le_ciSup_of_le, Exists.intro, Membership.mem, Set and 32 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  16. lemma MeasureTheory.SimpleFunc.iSup_nnapprox line 517 source

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

    Statement uses: MeasurableSpace, NNReal, Measurable, Eq, iSup, Nat, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.nnapprox

    Proof uses: funext, MeasureTheory.SimpleFunc.iSup_nnapprox_apply

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  17. theorem MeasureTheory.Measurable.nnreal_induction modelled after Measurable.ennreal_induction but with very raw assumptions line 527 source

    Source documentation

    modelled after Measurable.ennreal_induction but with very raw assumptions

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

    Statement uses: MeasurableSpace, NNReal, MeasureTheory.SimpleFunc, Measurable, Nat, MeasureTheory.SimpleFunc.nnapprox

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    protected theorem Measurable.nnreal_induction {α : Type*} {mα : MeasurableSpace α} {motive : (α → ℝ≥0) → Prop}
    (simpleFunc : ∀ ⦃f : SimpleFunc α ℝ≥0⦄, motive f)
    (approx :
      ∀ ⦃f : α → ℝ≥0⦄, (_ : Measurable f) → (∀ (n : ℕ), motive (SimpleFunc.nnapprox f n)) → motive f)
    ⦃f : α → ℝ≥0⦄ (hf : Measurable f) : motive f := by
…

    Mentions: MeasureTheory.SimpleFunc.nnapprox

  18. theorem MeasureTheory.Measurable.ennreal_induction' modified from ennreal_induction line 538 source

    Source comment

    modified from ennreal_induction

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

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.SimpleFunc, Nat, Monotone, iSup, Measurable

    Proof uses: Eq.mpr, MeasureTheory.SimpleFunc.eapprox, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, id, congrArg, MeasureTheory.SimpleFunc.iSup_eapprox_apply, MeasureTheory.SimpleFunc.monotone_eapprox

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    protected theorem Measurable.ennreal_induction' {α : Type*} {mα : MeasurableSpace α} {motive : (α → ℝ≥0∞) → Prop}
    (simpleFunc : ∀ ⦃f : SimpleFunc α ℝ≥0∞⦄, motive f)
    (iSup :
      ∀ ⦃f : ℕ → (SimpleFunc α ℝ≥0∞)⦄,
        Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x)
    ⦃f : α → ℝ≥0∞⦄ (hf : Measurable f) : motive f := by
…
  19. lemma MeasureTheory.Antitone.antitone_eapprox line 549 source

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

    Statement uses: TopologicalSpace, MeasurableSpace, BorelSpace, LinearOrder, OrderClosedTopology, ENNReal, Antitone, Nat, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.eapprox

    Proof uses: id, LE.le, Eq.mpr, MeasureTheory.SimpleFunc.approx, MeasureTheory.SimpleFunc.ennrealRatEmbed, Finset.sup, Finset.range, ite, Classical.propDecidable, OfNat.ofNat, Eq, congrArg, MeasureTheory.SimpleFunc.approx_apply, Antitone.measurable, Finset.sup_mono_fun, Membership.mem, Finset, dite, congrFun', ite_eq_left and 10 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  20. theorem MeasureTheory.Antitone.ennreal_induction' modified from ennreal_induction line 566 source

    Source comment

    modified from ennreal_induction

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

    Statement uses: TopologicalSpace, MeasurableSpace, BorelSpace, LinearOrder, OrderClosedTopology, ENNReal, MeasureTheory.SimpleFunc, Antitone, Nat, Monotone, iSup

    Proof uses: Eq.mpr, MeasureTheory.SimpleFunc.eapprox, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, id, congrArg, MeasureTheory.SimpleFunc.iSup_eapprox_apply, Antitone.measurable, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.Antitone.antitone_eapprox

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    protected theorem Antitone.ennreal_induction' {α : Type*} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [LinearOrder α] [OrderClosedTopology α]
   {motive : (α → ℝ≥0∞) → Prop}
    (simpleFunc : ∀ ⦃f : SimpleFunc α ℝ≥0∞⦄, Antitone f → motive f)
    (iSup :
      ∀ ⦃f : ℕ → (SimpleFunc α ℝ≥0∞)⦄,
        Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x)
    ⦃f : α → ℝ≥0∞⦄ (hf : Antitone f) : motive f := by
…