NNReal

📁 Source: Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean

Statistics

Metric	Count
Definitions	0
Theorems ext_of_integral_eq_on_compactlySupported_nnreal, integralLinearMap_inj, integralLinearMap_rieszMeasure, integral_rieszMeasure, lintegral_rieszMeasure, rieszMeasure_integralLinearMap, rieszMeasure_regular	7
Total	7

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_integral_eq_on_compactlySupported_nnreal 📖	—	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField NNReal.toReal DFunLike.coe CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace CompactlySupportedContinuousMap.instFunLike	—	—	ext_of_integral_eq_on_compactlySupported MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part CompactlySupportedContinuousMap.integrable BorelSpace.opensMeasurable Regular.toIsFiniteMeasureOnCompacts instIsTopologicalAddGroupReal

NNRealRMK

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integralLinearMap_inj 📖	mathematical	—	CompactlySupportedContinuousMap.integralLinearMap BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported_nnreal CompactlySupportedContinuousMap.toReal_apply CompactlySupportedContinuousMap.integralLinearMap_apply
integralLinearMap_rieszMeasure 📖	mathematical	—	CompactlySupportedContinuousMap.integralLinearMap BorelSpace.opensMeasurable rieszMeasure MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts rieszMeasure_regular	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.ext BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts rieszMeasure_regular NNReal.eq CompactlySupportedContinuousMap.toReal_apply integral_rieszMeasure CompactlySupportedContinuousMap.integralLinearMap_apply
integral_rieszMeasure 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField rieszMeasure NNReal.toReal DFunLike.coe CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace CompactlySupportedContinuousMap.instFunLike LinearMap NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.instFunLike	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal RealRMK.integral_rieszMeasure T2Space.r1Space MeasureTheory.Content.measure.congr_simp rieszContent.congr_simp CompactlySupportedContinuousMap.eq_toNNRealLinear_toRealPositiveLinear CompactlySupportedContinuousMap.toReal_apply
lintegral_rieszMeasure 📖	mathematical	—	MeasureTheory.lintegral rieszMeasure ENNReal.ofNNReal DFunLike.coe CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace CompactlySupportedContinuousMap.instFunLike LinearMap NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.instFunLike	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul MeasureTheory.lintegral_coe_eq_integral T2Space.r1Space rieszMeasure.eq_1 Continuous.integrable_of_hasCompactSupport BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Content.regular instWeaklyLocallyCompactSpaceOfLocallyCompactSpace Continuous.comp' NNReal.continuous_coe ContinuousMapClass.map_continuous CompactlySupportedContinuousMapClass.toContinuousMapClass CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass HasCompactSupport.comp_left CompactlySupportedContinuousMap.hasCompactSupport ENNReal.ofNNReal_toNNReal MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.toNNReal_of_nonneg NNReal.eq_iff integral_rieszMeasure
rieszMeasure_integralLinearMap 📖	mathematical	—	rieszMeasure CompactlySupportedContinuousMap.integralLinearMap BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts	—	MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported_nnreal BorelSpace.opensMeasurable MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts rieszMeasure_regular IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul CompactlySupportedContinuousMap.toReal_apply integral_rieszMeasure CompactlySupportedContinuousMap.integralLinearMap_apply
rieszMeasure_regular 📖	mathematical	—	MeasureTheory.Measure.Regular rieszMeasure	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul MeasureTheory.Content.regular T2Space.r1Space instWeaklyLocallyCompactSpaceOfLocallyCompactSpace

---

← Back to Index