Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem intervalIntegral.enorm_integral_min_max line 19 source

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

    Statement uses: NormedAddCommGroup, NormedSpace, Real, MeasureTheory.Measure, Eq, ENNReal, ENorm.enorm, intervalIntegral, Min.min, Max.max

    Proof uses: LE.le, Or, le_total, Or.inl, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, inf_of_le_left, sup_of_le_right, eq_self, Or.inr, Neg.neg, inf_of_le_right, sup_of_le_left, intervalIntegral.integral_symm, enorm_neg, Eq.refl

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. theorem intervalIntegral.enorm_integral_eq_enorm_integral_uIoc line 23 source

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

    Statement uses: NormedAddCommGroup, NormedSpace, Real, MeasureTheory.Measure, Eq, ENNReal, ENorm.enorm, intervalIntegral, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.uIoc

    Proof uses: Eq.mpr, Min.min, Max.max, id, congrArg, Eq.symm, intervalIntegral.enorm_integral_min_max, Set.Ioc, intervalIntegral.integral_of_le, min_le_max, Set, Set.uIoc.eq_1, Eq.refl

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem intervalIntegral.enorm_integral_le_lintegral_enorm_uIoc line 27 source

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

    Statement uses: NormedAddCommGroup, NormedSpace, Real, MeasureTheory.Measure, LE.le, ENNReal, ENorm.enorm, intervalIntegral, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.uIoc

    Proof uses: Trans.trans, Eq, MeasureTheory.integral, intervalIntegral.enorm_integral_eq_enorm_integral_uIoc, MeasureTheory.enorm_integral_le_lintegral_enorm

    23 instances, coercions and auxiliary constants left out.