PFR/ForMathlib/FiniteRange/IdentDistrib.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, Polynomial Freiman-Ruzsa proof paper, arXiv v2

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. lemma ProbabilityTheory.identDistrib_of_finiteRange If X has identical distribution to X₀, and X₀ has finite range, then X is almost everywhere equivalent to a random variable of finite range line 24 source

    Source documentation

    If X has identical distribution to X₀, and X₀ has finite range, then X is almost everywhere equivalent to a random variable of finite range.

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Nonempty, MeasureTheory.Measure, FiniteRange, Measurable, ProbabilityTheory.IdentDistrib, Exists, And, Filter.EventuallyEq, MeasureTheory.ae

    Proof uses: Finset, FiniteRange.toFinset, ite, Membership.mem, Classical.propDecidable, Eq, Nonempty.some, Exists.intro, And.intro, Measurable.ite, MeasurableSet.preimage, Finset.measurableSet, measurable_const, finiteRange_of_finset, Union.union, Singleton.singleton, Eq.mpr, Or, id, Eq.trans and 43 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

    lemma identDistrib_of_finiteRange {Ω Ω₀ S : Type*}
    [MeasurableSpace Ω] [MeasurableSpace Ω₀] [MeasurableSpace S] [MeasurableSingletonClass S]
    [hS : Nonempty S] {μ : Measure Ω} {μ₀ : Measure Ω₀} {X₀ : Ω₀ → S} [FiniteRange X₀] {X : Ω → S}
    (hX : Measurable X) (hi : IdentDistrib X₀ X μ₀ μ) :
    ∃ X' : Ω → S, Measurable X' ∧ FiniteRange X' ∧ X' =ᵐ[μ] X := by
…

    Mentions: FiniteRange

  2. lemma ProbabilityTheory.independent_copies_finiteRange A version of independent_copies that guarantees that the copies have FiniteRange if the original variables do line 50 source

    Source documentation

    A version of independent_copies that guarantees that the copies have FiniteRange if the original variables do.

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

    Statement uses: MeasurableSpace, Measurable, FiniteRange, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, Prod, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib

    Proof uses: Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, ProbabilityTheory.independent_copies, Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.identDistrib_of_finiteRange, ProbabilityTheory.IdentDistrib.symm, Exists.intro, And.intro, ProbabilityTheory.IndepFun.congr, Filter.EventuallyEq.symm, Eq.mpr, Eq.refl, ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.IdentDistrib.of_ae_eq, Measurable.aemeasurable

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

    lemma independent_copies_finiteRange {X : Ω → α} {Y : Ω' → β}
    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y]
    [MeasurableSingletonClass α] [MeasurableSingletonClass β]
    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃
    Y' : α × β → β, IsProbabilityMeasure ν
      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν
      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' ∧ FiniteRange X' ∧ FiniteRange Y' := by
…

    Mentions: FiniteRange

  3. lemma ProbabilityTheory.independent_copies3_nondep_finiteRange A version of independent_copies3_nondep that guarantees that the copies have FiniteRange if the original variables do line 73 source

    Source documentation

    A version of independent_copies3_nondep that guarantees that the copies have FiniteRange if the original variables do.

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib

    Proof uses: Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, ProbabilityTheory.independent_copies3_nondep, Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.identDistrib_of_finiteRange, ProbabilityTheory.IdentDistrib.symm, Exists.intro, And.intro, ProbabilityTheory.iIndepFun.ae_eq, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete and 18 more

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

    lemma independent_copies3_nondep_finiteRange {α : Type u}
    [mS : MeasurableSpace α] [MeasurableSingletonClass α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃)
    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃]
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃)
    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂]
    [hμ₃ : IsProbabilityMeasure μ₃] :
    ∃ (A : Type (max u_1 u_2 u_3)) (_ : MeasurableSpace A) (μA : Measure A)
      (X₁' X₂' X₃' : A → α),
…

    Mentions: FiniteRange

  4. lemma ProbabilityTheory.independent_copies4_nondep_finiteRange A version of independent_copies4_nondep that guarantees that the copies have FiniteRange if the original variables do line 110 source

    Source documentation

    A version of independent_copies4_nondep that guarantees that the copies have FiniteRange if the original variables do.

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib

    Proof uses: Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, ProbabilityTheory.independent_copies4_nondep, Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.identDistrib_of_finiteRange, ProbabilityTheory.IdentDistrib.symm, Exists.intro, And.intro, ProbabilityTheory.iIndepFun.ae_eq, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete and 18 more

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

    lemma independent_copies4_nondep_finiteRange {α : Type u}
    [mS : MeasurableSpace α] [MeasurableSingletonClass α]
    {Ω₁ : Type u_1} {Ω₂ : Type u_2} {Ω₃ : Type u_3} {Ω₄ : Type u_4}
    [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃] [MeasurableSpace Ω₄]
    {X₁ : Ω₁ → α} {X₂ : Ω₂ → α} {X₃ : Ω₃ → α} {X₄ : Ω₄ → α}
    (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hX₄ : Measurable X₄)
    [FiniteRange X₁] [FiniteRange X₂] [FiniteRange X₃] [FiniteRange X₄]
    (μ₁ : Measure Ω₁) (μ₂ : Measure Ω₂) (μ₃ : Measure Ω₃) (μ₄ : Measure Ω₄)
    [hμ₁ : IsProbabilityMeasure μ₁] [hμ₂ : IsProbabilityMeasure μ₂] [hμ₃ : IsProbabilityMeasure μ₃]
    [hμ₄ : IsProbabilityMeasure μ₄] :
    ∃ (A : Type (max u_1 u_2 u_3 u_4)) (_ : MeasurableSpace A) (μA : Measure A)
      (X₁' X₂' X₃' X₄' : A → α),
…

    Mentions: FiniteRange

  5. lemma ProbabilityTheory.independent_copies'_finiteRange A version of independent_copies' that guarantees that the copies have FiniteRange if the original variables do line 153 source

    Source documentation

    A version of independent_copies' that guarantees that the copies have FiniteRange if the original variables do.

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

    Statement uses: Finite, MeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Exists, And, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib

    Proof uses: Fintype, Eq, nonempty_fintype, Nonempty.intro, ProbabilityTheory.independent_copies', Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.identDistrib_of_finiteRange, And.left, ProbabilityTheory.IdentDistrib.symm, And.right, Exists.intro, And.intro, ProbabilityTheory.iIndepFun.ae_eq, Filter.EventuallyEq.symm, ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.IdentDistrib.of_ae_eq, Measurable.aemeasurable, Classical.choose, Classical.choose_spec and 1 more

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma independent_copies'_finiteRange {I : Type u} [Finite I] {α : I → Type u'}
    [mS : ∀ i : I, MeasurableSpace (α i)] [mS' : ∀ i, MeasurableSingletonClass (α i)]
    [mnon: ∀ i, Nonempty (α i)] {Ω : I → Type v}
    [mΩ : ∀ i : I, MeasurableSpace (Ω i)] (X : ∀ i : I, Ω i → α i) (hX : ∀ i : I, Measurable (X i))
    (μ : ∀ i : I, Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] [∀ i, FiniteRange (X i)] :
    ∃ (A : Type (max u v)) (_ : MeasurableSpace A) (μA : Measure A) (X' : ∀ i, A → α i),
    IsProbabilityMeasure μA ∧ iIndepFun X' μA ∧
    ∀ i : I, Measurable (X' i) ∧ IdentDistrib (X' i) (X i) μA (μ i) ∧ FiniteRange (X' i) := by
…

    Mentions: FiniteRange