PFR/Mathlib/MeasureTheory/Measure/Prod.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 (1)
Imported by 2 files
  1. lemma MeasureTheory.Measure.map_prod_comap_swap The law of $(X, Z)$ is the image of the law of $(Z,X)$ line 15 source

    Source documentation

    The law of $(X, Z)$ is the image of the law of $(Z,X)$.

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

    Statement uses: MeasurableSpace, Measurable, MeasureTheory.Measure, Eq, Prod, MeasureTheory.Measure.comap, Prod.swap, MeasureTheory.Measure.map, Prod.mk

    Proof uses: MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Measurable.prodMk, Set.image, MeasureTheory.Measure.comap_apply, Prod.swap_injective, MeasurableEmbedding.measurableSet_image', MeasurableEquiv, MeasurableEquiv.prodComm, MeasurableEquiv.measurableEmbedding, eq_of_heq, outParam, DFunLike and 15 more

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma map_prod_comap_swap (hX : Measurable X) (hZ : Measurable Z) (μ : Measure Ω) :
    (μ.map (fun ω ↦ (X ω, Z ω))).comap Prod.swap = μ.map (fun ω ↦ (Z ω, X ω)) := by
…
  2. lemma MeasureTheory.Measure.prod_apply_singleton line 26 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Prod, Eq, ENNReal, Set, MeasureTheory.Measure.prod, Singleton.singleton, HMul.hMul, Prod.fst, Prod.snd

    Proof uses: Eq.mpr, Prod.mk, id, congrArg, Eq.symm, Prod.eta, SProd.sprod, Set.singleton_prod_singleton, MeasureTheory.Measure.prod_prod, Eq.refl

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma MeasureTheory.Measure.prod_real_apply_singleton line 31 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Prod, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.prod, Singleton.singleton, Set, HMul.hMul, Prod.fst, Prod.snd

    Proof uses: of_eq_true, ENNReal.toReal, ENNReal, Eq.trans, True, congrFun', congrArg, MeasureTheory.Measure.prod_apply_singleton, ENNReal.toReal_mul, eq_self

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma MeasureTheory.Measure.prod_of_full_measure_finset line 36 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, Prod, MeasureTheory.Measure.prod, SProd.sprod

    Proof uses: Union.union, Set.univ, Set.ext, Iff, Membership.mem, Eq.mpr, Prod.mk, Not, Or, id, congr, congrArg, Eq.trans, congrFun', Finset.coe_product, And, Prod.fst, Prod.snd, True, and_true and 16 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  5. instance (instance at line 49) line 49 source