Carleson/ToMathlib/MeasureTheory/Function/LocallyIntegrable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem MeasureTheory.LocallyIntegrable.norm line 13 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, NormedAddCommGroup, MeasureTheory.Measure, MeasureTheory.LocallyIntegrable, Real, Norm.norm

    Proof uses: MeasureTheory.IntegrableAtFilter.norm, nhds

    19 instances, coercions and auxiliary constants left out.

  2. theorem MeasureTheory.LocallyIntegrable.congr'_enorm line 22 source

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

    Statement uses: MeasurableSpace, TopologicalSpace, ContinuousENorm, MeasureTheory.Measure, MeasureTheory.LocallyIntegrable, MeasureTheory.AEStronglyMeasurable, Filter.Eventually, Eq, ENNReal, ENorm.enorm, MeasureTheory.ae

    Proof uses: MeasureTheory.IntegrableAtFilter.congr'_enorm, nhds

    6 instances, coercions and auxiliary constants left out.