Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. lemma MeasureTheory.eLpNormEssSup_congr_measure line 19 source

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

    Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, Filter, MeasureTheory.ae, ENNReal, MeasureTheory.eLpNormEssSup

    Proof uses: id, essSup, ENorm.enorm, ConditionallyCompleteLattice, Eq.rec, Filter.limsup, Eq.refl

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma MeasureTheory.eLpNormEssSup_withDensity line 24 source

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

    Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, AEMeasurable, Filter.Eventually, Ne, OfNat.ofNat, MeasureTheory.ae, Eq, MeasureTheory.eLpNormEssSup, MeasureTheory.Measure.withDensity

    Proof uses: MeasureTheory.eLpNormEssSup_congr_measure, le_antisymm, Filter, Eq.mpr, LE.le, MeasureTheory.Measure.AbsolutelyContinuous, id, congrArg, propext, MeasureTheory.Measure.ae_le_iff_absolutelyContinuous, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.withDensity_absolutelyContinuous'

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  3. lemma MeasureTheory.eLpNormEssSup_nnreal_scale_constant' line 34 source

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

    Statement uses: NNReal, ENNReal, Ne, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Eq, MeasureTheory.eLpNormEssSup, HMul.hMul

    Proof uses: Trans.trans, Function.comp, rfl, MeasurableSpace, ENorm, Eq.rec, MeasureTheory.Measure, Eq.refl, Eq.mpr, MeasureTheory.Measure.map, id, congrArg, Eq.symm, MeasureTheory.eLpNormEssSup_map_measure, HSMul.hSMul, Inv.inv, NNReal.map_volume_mul_left, MeasureTheory.AEStronglyMeasurable.smul_measure, AEMeasurable.const_mul, aemeasurable_id and 6 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  4. lemma MeasureTheory.eLpNorm_withDensity_scale_constant' line 46 source

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

    Statement uses: NNReal, ENNReal, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Ne, OfNat.ofNat, Eq, MeasureTheory.eLpNorm, HMul.hMul, MeasureTheory.Measure.withDensity, Inv.inv

    Proof uses: id, dite, ite, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, Eq.mpr, congr, congrArg, ite_eq_left, Eq.refl, Not, ite_eq_right, MeasureTheory.eLpNormEssSup_withDensity, AEMeasurable.fun_inv, AEMeasurable.coe_nnreal_ennreal, aemeasurable_id, of_eq_true, Filter.Eventually and 41 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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