Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Some tools for measure theory computations

A collection of small lemmas to help with integral manipulations.

Imports (1)
Imported by 2 files
  1. lemma MeasureTheory.measure_preserving_shift line 21 source

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

    Statement uses: Real, MeasureTheory.MeasurePreserving, HAdd.hAdd, MeasureTheory.MeasureSpace.volume

    Proof uses: MeasureTheory.measurePreserving_add_left

    32 instances, coercions and auxiliary constants left out.

  2. lemma MeasureTheory.measureable_embedding_shift line 25 source

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

    Statement uses: Real, MeasurableEmbedding, HAdd.hAdd

    Proof uses: measurableEmbedding_addLeft

    25 instances, coercions and auxiliary constants left out.

  3. lemma MeasureTheory.measure_preserving_scaling line 28 source

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

    Statement uses: Real, Ne, OfNat.ofNat, MeasureTheory.MeasurePreserving, HMul.hMul, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, ENNReal, MeasureTheory.Measure, ENNReal.ofReal, abs, Inv.inv

    Proof uses: MeasureTheory.MeasurePreserving.mk, MeasurableMul.measurable_const_mul, Real.map_volume_mul_left

    51 instances, coercions and auxiliary constants left out.

  4. lemma MeasureTheory.lintegral_shift line 32 source

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

    Statement uses: Real, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, HAdd.hAdd

    Proof uses: MeasureTheory.lintegral_add_right_eq_self

    37 instances, coercions and auxiliary constants left out.

  5. lemma MeasureTheory.lintegral_shift' line 36 source

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

    Statement uses: Real, ENNReal, Set, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.preimage, HAdd.hAdd

    Proof uses: Eq.mpr, id, congrArg, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb, MeasureTheory.measurePreserving_add_right, measurableEmbedding_addRight, Eq.refl

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. lemma MeasureTheory.lintegral_add_right_Ioi line 41 source

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

    Statement uses: Real, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HSub.hSub, HAdd.hAdd

    Proof uses: Eq.mpr, Set.preimage, id, congrArg, Eq.symm, MeasureTheory.lintegral_shift', of_eq_true, Eq.trans, True, congrFun', MeasureTheory.Measure, Set, Set.preimage_add_const_Ioi, eq_self

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  7. lemma MeasureTheory.lintegral_scale_constant line 46 source

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

    Statement uses: Real, ENNReal, Ne, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, HMul.hMul, ENNReal.ofReal, abs, Inv.inv

    Proof uses: Eq.mpr, HSMul.hSMul, id, congrArg, Eq.symm, smul_eq_mul, MeasureTheory.Measure, MeasureTheory.lintegral_smul_measure, MeasureTheory.MeasurePreserving.lintegral_comp_emb, MeasureTheory.measure_preserving_scaling, measurableEmbedding_mulLeft₀, Eq.refl

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  8. lemma MeasureTheory.lintegral_scale_constant_preimage line 52 source

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

    Statement uses: Real, ENNReal, Ne, OfNat.ofNat, Set, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.preimage, HMul.hMul, ENNReal.ofReal, abs, Inv.inv

    Proof uses: Eq.mpr, HSMul.hSMul, id, congrArg, Eq.symm, smul_eq_mul, MeasureTheory.Measure, MeasureTheory.lintegral_smul_measure, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb, MeasureTheory.measure_preserving_scaling, measurableEmbedding_mulLeft₀, MeasureTheory.Measure.restrict_smul, Eq.refl

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. lemma MeasureTheory.lintegral_scale_constant_halfspace line 58 source

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

    Statement uses: Real, ENNReal, LT.lt, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HMul.hMul, ENNReal.ofReal, abs, Inv.inv

    Proof uses: Eq.mpr, Set.preimage, id, congrArg, Eq.symm, MeasureTheory.lintegral_scale_constant_preimage, LT.lt.ne', Set, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, propext, mul_pos_iff_of_pos_left, iff_self, Eq.refl

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  10. lemma MeasureTheory.lintegral_scale_constant_halfspace' line 66 source

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

    Statement uses: Real, ENNReal, LT.lt, OfNat.ofNat, Eq, HMul.hMul, ENNReal.ofReal, abs, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi

    Proof uses: Eq.mpr, Inv.inv, id, congrArg, MeasureTheory.lintegral_scale_constant_halfspace, Eq.symm, mul_assoc, ENNReal.ofReal_mul, abs_nonneg, LE.le, abs_inv, mul_inv_cancel₀, Iff.mpr, Ne, abs_ne_zero, LT.lt.ne', of_eq_true, Eq.trans, True, congrFun' and 3 more

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  11. lemma MeasureTheory.lintegral_scale_constant' line 72 source

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

    Statement uses: Real, ENNReal, Ne, OfNat.ofNat, Eq, HMul.hMul, ENNReal.ofReal, abs, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume

    Proof uses: Eq.mpr, Inv.inv, id, congrArg, MeasureTheory.lintegral_scale_constant, Eq.symm, mul_assoc, ENNReal.ofReal_mul, abs_nonneg, LE.le, abs_inv, mul_inv_cancel₀, Iff.mpr, abs_ne_zero, of_eq_true, Eq.trans, True, congrFun', ENNReal.ofReal_one, one_mul and 1 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  12. lemma MeasureTheory.lintegral_set_mono_fn line 81 source

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, MeasurableSet, ENNReal, Membership.mem, LE.le, MeasureTheory.lintegral, MeasureTheory.Measure.restrict

    Proof uses: Eq.mpr, Set.indicator, id, Eq, congrArg, Eq.symm, MeasureTheory.lintegral_indicator, MeasureTheory.lintegral_mono, Decidable, ite, Classical.decPred, OfNat.ofNat, Not, congr, ite_eq_right, le_refl, ite_eq_left

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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