PFR/Mathlib/Probability/Independence/Basic.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

19 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 4 files
  1. lemma ProbabilityTheory.IndepFun.measureReal_inter_preimage_eq_mul line 16 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IndepFun, Set, MeasurableSet, Eq, Real, MeasureTheory.Measure.real, Inter.inter, Set.preimage, HMul.hMul

    Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul, ENNReal.toReal_mul, Eq.refl

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma ProbabilityTheory.iIndepFun.inv line 39 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Inv, MeasurableInv, DecidableEq, ProbabilityTheory.iIndepFun, Function.update, Inv.inv

    Proof uses: Eq.mpr, Function.comp, id, eq_of_heq, Eq, autoParam, HEq, Eq.refl, HEq.refl, Eq.symm, funext, dite, of_eq_true, Eq.trans, True, congr, congrArg, congrFun, Function.update_self, congrFun' and 9 more

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  3. lemma ProbabilityTheory.iIndepFun.finsets Documented declaration: finsets line 52 source

    Source documentation

    If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint finite index sets, then the tuples formed by f i for i ∈ S j are mutually independent, when seen as a family indexed by J.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Set.PairwiseDisjoint, Set.univ, ProbabilityTheory.iIndepFun, Measurable, Subtype, Membership.mem

    Proof uses: ProbabilityTheory.Kernel.iIndepFun.finsets, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Unit.unit

    9 instances, coercions and auxiliary constants left out.

    lemma iIndepFun.finsets {f : ∀ i, Ω → β i} {J : Type*}
    (S : J → Finset ι) (h_disjoint : Set.PairwiseDisjoint Set.univ S)
    (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) :
    iIndepFun (fun (j : J) ↦ fun a (i : S j) ↦ f i a) μ :=
…
  4. lemma ProbabilityTheory.iIndepFun.finsets_comp Documented declaration: finsets_comp line 62 source

    Source documentation

    If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint finite index sets, and φ j is a function that maps the tuple formed by f i for i ∈ S j to a measurable space γ j, then the family of random variables formed by φ j (f i)_{i ∈ S j} and indexed by J is iIndep.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Set.PairwiseDisjoint, Set.univ, ProbabilityTheory.iIndepFun, Measurable, Subtype, Membership.mem

    Proof uses: ProbabilityTheory.Kernel.iIndepFun.finsets_comp, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Unit.unit

    13 instances, coercions and auxiliary constants left out.

    lemma iIndepFun.finsets_comp {f : ∀ i, Ω → β i} {J : Type*}
    (S : J → Finset ι) (h_disjoint : Set.PairwiseDisjoint Set.univ S)
    (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i))
    {γ : J → Type*} {mγ : ∀ j, MeasurableSpace (γ j)}
    (φ : (j : J) → ((i : S j) → β i) → γ j) (hφ : ∀ j, Measurable (φ j)) :
    iIndepFun (fun (j : J) ↦ fun a ↦ φ j (fun (i : S j) ↦ f i a)) μ :=
…
  5. lemma ProbabilityTheory.iIndepFun.finsetSum line 70 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommMonoid, MeasurableAdd₂, Finset, Set.PairwiseDisjoint, Set.univ, ProbabilityTheory.iIndepFun, Measurable, Finset.sum

    Proof uses: Subtype, Membership.mem, Finset.univ, Eq, rfl, Eq.mpr, id, congrArg, Finset.measurable_sum, Finset.attach, measurable_pi_apply, ProbabilityTheory.iIndepFun.finsets_comp, of_eq_true, Eq.trans, True, congr, congrFun', congrFun, Finset.sum_congr, Eq.refl and 6 more

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  6. lemma ProbabilityTheory.IndepFun.finsetSum line 85 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommMonoid, MeasurableAdd₂, Finset, ProbabilityTheory.iIndepFun, Measurable, Disjoint, ProbabilityTheory.IndepFun, Finset.sum

    Proof uses: Bool, ite, Eq, Bool.true, Set.PairwiseDisjoint, Set.univ, Membership.mem, Set, Ne, dite, Function.onFun, False.elim, Eq.rec, Eq.symm, Not, Eq.mpr, id, congr, congrArg, Eq.trans and 21 more

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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

  7. lemma ProbabilityTheory.iIndepFun.finsets_comp' A variant of iIndepFun.finsets_comp where we conclude the independence of just two functions rather than an entire family line 108 source

    Source documentation

    A variant of iIndepFun.finsets_comp where we conclude the independence of just two functions rather than an entire family.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Disjoint, ProbabilityTheory.iIndepFun, Measurable, Subtype, Membership.mem, ProbabilityTheory.IndepFun

    Proof uses: Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Unit, Set.PairwiseDisjoint, Set.univ, id, Set.Pairwise, Function.onFun, Eq.mpr, Set, Ne, And, Eq, Eq.trans, forall_congr, implies_congr and 19 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    lemma iIndepFun.finsets_comp' {f : ∀ i, Ω → β i} {S S' : Finset ι} (h_disjoint : Disjoint S S')
    (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i))
    {γ γ' : Type u} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'}
    {φ : (∀ i : S, β i) → γ} {φ' : (∀ i : S', β i) → γ'} (hφ : Measurable φ) (hφ' : Measurable φ') :
    IndepFun (fun a ↦ φ (fun (i : S) ↦ f i a)) (fun a ↦ φ' (fun (i : S') ↦ f i a)) μ := by
…
  8. lemma ProbabilityTheory.indepFun_zero_measure line 137 source

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

    Statement uses: MeasurableSpace, ProbabilityTheory.IndepFun, OfNat.ofNat, MeasureTheory.Measure

    Proof uses: of_eq_true, ProbabilityTheory.Kernel.IndepFun, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Unit.unit, Eq.trans, ProbabilityTheory.Kernel, True, congrFun', congrArg, autoParam, ProbabilityTheory.Kernel.const_zero

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. lemma ProbabilityTheory.indepFun_const Random variables are always independent of constants line 141 source

    Source documentation

    Random variables are always independent of constants.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.IndepFun

    Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.symm, Eq.mpr, Set, MeasurableSet, MeasurableSpace.comap, ENNReal, Inter.inter, HMul.hMul, id, congrArg, propext, ProbabilityTheory.IndepFun_iff, Bot.bot, MeasurableSpace.comap_const and 14 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    lemma indepFun_const [IsZeroOrProbabilityMeasure μ] (c : α) : IndepFun f (fun _ => c) μ := by
…
  10. lemma ProbabilityTheory.indepFun_fst_snd line 149 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.IndepFun, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod

    Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congrArg, MeasureTheory.Measure.zero_prod, Eq.symm, MeasureTheory.Measure.prod_zero, Eq.mpr, Set, MeasurableSet, MeasurableSpace.comap, ENNReal, Inter.inter, HMul.hMul, id and 16 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  11. lemma ProbabilityTheory.IndepFun.comp_right Composing independent functions with a measurable embedding of conull range gives independent functions line 163 source

    Source documentation

    Composing independent functions with a measurable embedding of conull range gives independent functions.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableEmbedding, Filter.Eventually, Membership.mem, Set, Set.range, MeasureTheory.ae, Measurable, ProbabilityTheory.IndepFun, Function.comp, MeasureTheory.Measure.comap

    Proof uses: id, Eq, ENNReal, Compl.compl, OfNat.ofNat, Eq.mpr, MeasurableSet, MeasurableSpace.comap, Inter.inter, HMul.hMul, congrArg, propext, ProbabilityTheory.IndepFun_iff, And, Set.preimage, Set.preimage_comp, Eq.symm, Set.preimage_inter, Set.image, MeasureTheory.Measure.comap_apply and 11 more

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    lemma IndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) (hg : Measurable g) (hfg : IndepFun f g μ) :
    IndepFun (f ∘ i) (g ∘ i) (μ.comap i) := by
…
  12. lemma ProbabilityTheory.iIndepFun_iff' Same as iIndepFun_iff except that the function f' returns measurable sets even on junk values line 181 source

    Source comment

    Same as `iIndepFun_iff` except that the function `f'` returns measurable sets even on junk values

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Iff, ProbabilityTheory.iIndepFun, Finset, Set, MeasurableSet, MeasurableSpace.comap, Eq, ENNReal, Set.iInter, Membership.mem, Finset.prod

    Proof uses: Eq.mpr, id, congrArg, propext, ProbabilityTheory.iIndepFun_iff, forall_congr', Iff.intro, ite, Classical.propDecidable, Set.univ, Eq.symm, ite_eq_left, eq_of_heq, HEq, Eq.refl, HEq.refl, outParam, DFunLike, Set.iInter₂_congr, Finset.prod_congr and 9 more

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma iIndepFun_iff' [MeasurableSpace Ω] {β : ι → Type*}
    (m : ∀ i, MeasurableSpace (β i)) (f : ∀ i, Ω → β i) (μ : Measure Ω) :
    iIndepFun f μ ↔ ∀ (s : Finset ι) ⦃f' : ι → Set Ω⦄
      (_hf' : ∀ i, MeasurableSet[(m i).comap (f i)] (f' i)),
      μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i) := by
…
  13. lemma ProbabilityTheory.measurable_sigmaCurry line 204 source

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

    Statement uses: MeasurableSpace, Measurable, Sigma, Sigma.fst, Sigma.snd, Sigma.curry

    Proof uses: measurable_sigmaCurry

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  14. lemma ProbabilityTheory._root_.Finset.prod_univ_prod line 212 source
  15. lemma ProbabilityTheory._root_.Finset.prod_univ_prod' line 217 source
  16. lemma ProbabilityTheory.iIndepFun.pi If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent line 226 source

    Source documentation

    If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, Measurable, ProbabilityTheory.iIndepFun, Sigma, Sigma.fst, Sigma.snd

    Proof uses: Fintype, Fintype.ofFinite, Set, Set.image, Set.pi, Set.univ, Set.ofPred, MeasurableSet, ProbabilityTheory.iIndepSets.iIndep, MeasurableSpace.comap, Iff.mp, LE.le, measurable_iff_comap_le, Iff.mpr, measurable_pi_iff, Exists, And, Membership.mem, Eq, Set.preimage and 70 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 57 steps

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

    lemma iIndepFun.pi
    (f_meas : ∀ i j, Measurable (f i j))
    (hf : iIndepFun (fun ij : Σ i, κ i ↦ f ij.1 ij.2) μ) :
    iIndepFun (fun i ω j ↦ f i j ω) μ := by
…
  17. lemma ProbabilityTheory.iIndepFun.pi' If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent line 284 source

    Source documentation

    If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, Sigma, Sigma.fst, Sigma.snd, Measurable, ProbabilityTheory.iIndepFun, Sigma.mk

    Proof uses: ProbabilityTheory.iIndepFun.pi

    1 instances, coercions and auxiliary constants left out.

    lemma iIndepFun.pi' {f : ∀ ij : (Σ i, κ i), Ω → α ij.1 ij.2 }
    (f_meas : ∀ i, Measurable (f i))
    (hf : iIndepFun f μ) :
    iIndepFun (fun i ω ↦ (fun j ↦ f ⟨i, j⟩ ω)) μ :=
…
  18. lemma ProbabilityTheory.iIndepFun.prod line 293 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Measurable, Finset, Pairwise, Function.onFun, Disjoint, ProbabilityTheory.iIndepFun, Subtype, Membership.mem

    Proof uses: Sigma, Function.dcomp, Sigma.fst, Sigma.snd, Function.Injective, Eq, Not, Iff.mpr, LE.le, Bot.bot, Exists, Classical.not_forall, Exists.intro, Singleton.singleton, Eq.mpr, And, id, Eq.trans, congrArg, implies_congr and 9 more

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  19. theorem ProbabilityTheory.iIndepFun.ae_eq TODO: a kernel version of this theorem line 312 source

    Source documentation

    TODO: a kernel version of this theorem

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.iIndepFun, Filter.EventuallyEq, MeasureTheory.ae

    Proof uses: Eq.mpr, ProbabilityTheory.iIndep, MeasurableSpace.comap, id, Eq, congrArg, propext, ProbabilityTheory.iIndepFun_iff_iIndep, Finset, Set, Membership.mem, MeasurableSet, ENNReal, Set.iInter, Finset.prod, ProbabilityTheory.iIndep_iff, Exists, And, Filter.EventuallyEqSet, dite and 26 more

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

    theorem iIndepFun.ae_eq {ι : Type*} {β : ι → Type*}
    {m : ∀ i, MeasurableSpace (β i)} {f g : ∀ i, Ω → β i}
    (hf_Indep : iIndepFun f μ) (hfg : ∀ i, f i =ᵐ[μ] g i) : iIndepFun g μ := by
…