PFR/Mathlib/MeasureTheory/Measure/Real.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. lemma MeasureTheory.Measure.ennreal_smul_real_apply line 15 source

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

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, Set, Eq, Real, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal.toReal

    Proof uses: of_eq_true, HMul.hMul, Eq.trans, True, congrFun', congrArg, MeasureTheory.measureReal_ennreal_smul_apply, eq_self

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma MeasureTheory.Measure.nnreal_smul_real_apply line 18 source

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

    Statement uses: MeasurableSpace, NNReal, MeasureTheory.Measure, Set, Eq, Real, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal

    Proof uses: of_eq_true, HMul.hMul, ENNReal.toReal, Eq.trans, True, congrFun', congrArg, ENNReal.toReal_mul, eq_self

    27 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.comap_real_apply line 21 source

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

    Statement uses: MeasurableSpace, Set, Function.Injective, MeasurableSet, Set.image, MeasureTheory.Measure, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.comap

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

    2 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_real_singleton line 25 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.

  5. lemma MeasureTheory.measureReal_preimage_fst_singleton_eq_sum line 31 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Fintype, MeasureTheory.Measure, Prod, MeasureTheory.IsFiniteMeasure, Eq, Real, MeasureTheory.Measure.real, Set.preimage, Prod.fst, Singleton.singleton, Set, Finset.sum, Finset.univ, Prod.mk

    Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, MeasureTheory.measure_preimage_fst_singleton_eq_sum, ENNReal.toReal_sum, Membership.mem, Finset, MeasureTheory.measure_ne_top, Eq.refl

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. lemma MeasureTheory.measureReal_preimage_snd_singleton_eq_sum line 39 source

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

    Statement uses: MeasurableSpace, MeasurableSingletonClass, Fintype, MeasureTheory.Measure, Prod, MeasureTheory.IsFiniteMeasure, Eq, Real, MeasureTheory.Measure.real, Set.preimage, Prod.snd, Singleton.singleton, Set, Finset.sum, Finset.univ, Prod.mk

    Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, MeasureTheory.measure_preimage_snd_singleton_eq_sum, ENNReal.toReal_sum, Membership.mem, Finset, MeasureTheory.measure_ne_top, Eq.refl

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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