AEEqOfLIntegral

📁 Source: Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_eq_of_forall_setLIntegral_eq, ae_const_le_iff_forall_lt_measure_zero, ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀, ae_eq_of_setLIntegral_prod_eq, ae_le_const_iff_forall_gt_measure_zero, ae_le_of_forall_setLIntegral_le_of_sigmaFinite, ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀, lintegral_eq_lintegral_of_isPiSystem, lintegral_eq_lintegral_of_isPiSystem_of_univ_mem, withDensity_eq_iff, withDensity_eq_iff_of_sigmaFinite	12
Total	12

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_const_le_iff_forall_lt_measure_zero 📖	mathematical	—	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass DFunLike.coe Set ENNReal setOf instZeroENNReal	—	Measure.instOuterMeasureClass ae_iff measure_mono_null lt_of_le_of_lt Set.eq_empty_iff_forall_notMem lt_irrefl lt_of_lt_of_le measure_empty le_of_lt IsLUB.exists_seq_strictMono_tendsto_of_notMem FirstCountableTopology.nhds_generated_countable Mathlib.Tactic.Push.not_forall_eq Set.ext Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_order LT.lt.le LE.le.trans_lt measure_iUnion_null_iff instCountableNat
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace lintegral Measure.restrict	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ Measurable.aemeasurable
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace lintegral Measure.restrict	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ le_of_eq ge_of_eq Filter.mp_mem Filter.univ_mem' le_antisymm
ae_eq_of_setLIntegral_prod_eq 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Prod.instMeasurableSpace lintegral Measure.restrict SProd.sprod Set Set.instSProd	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	setLIntegral_univ Set.univ_prod_univ MeasurableSet.univ AEMeasurable.ae_eq_of_forall_setLIntegral_eq lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod isPiSystem_prod
ae_le_const_iff_forall_gt_measure_zero 📖	mathematical	—	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass DFunLike.coe Set ENNReal setOf instZeroENNReal	—	ae_const_le_iff_forall_lt_measure_zero instOrderTopologyOrderDual instFirstCountableTopologyOrderDual
ae_le_of_forall_setLIntegral_le_of_sigmaFinite 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ Measurable.aemeasurable
ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	LE.le.trans_lt measure_mono Measure.instOuterMeasureClass Set.inter_subset_right measure_spanningSets_lt_top lintegral_const Measure.restrict_apply Set.univ_inter lintegral_add_right measurable_const setLIntegral_mono_ae AEMeasurable.restrict ae_of_all add_zero Measure.restrict_toMeasurable LT.lt.ne measurableSet_toMeasurable measure_toMeasurable setLIntegral_lt_top_of_le_nnreal ENNReal.le_of_add_le_add_left ENNReal.instCanonicallyOrderedAdd ENNReal.instNoZeroDivisors LT.lt.ne' exists_seq_strictAnti_tendsto NNReal.instOrderTopology NNReal.instDenselyOrdered IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.Tendsto.add ENNReal.instContinuousAdd tendsto_const_nhds ENNReal.tendsto_coe Filter.Tendsto.eventually_le_const instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.tendsto_nat_nhds_top Filter.Tendsto.eventually_const_le instClosedIicTopology LT.lt.trans_le le_top Set.mem_iUnion Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.and eventually_mem_spanningSets le_antisymm measure_iUnion_le instCountableNat tsum_zero bot_le
lintegral_eq_lintegral_of_isPiSystem 📖	—	MeasurableSpace.generateFrom IsPiSystem lintegral Measure.restrict MeasurableSet	—	—	MeasurableSpace.induction_on_inter Measure.restrict_empty lintegral_zero_measure setLIntegral_compl ne_of_lt setLIntegral_le_lintegral Ne.lt_top lintegral_iUnion instCountableNat
lintegral_eq_lintegral_of_isPiSystem_of_univ_mem 📖	—	MeasurableSpace.generateFrom IsPiSystem Set Set.instMembership Set.univ lintegral Measure.restrict MeasurableSet	—	—	lintegral_eq_lintegral_of_isPiSystem setLIntegral_univ
withDensity_eq_iff 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.withDensity Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass AEMeasurable.ae_eq_of_forall_setLIntegral_eq setLIntegral_univ withDensity_apply MeasurableSet.univ withDensity_congr_ae
withDensity_eq_iff_of_sigmaFinite 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.withDensity Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ withDensity_apply withDensity_congr_ae

MeasureTheory.AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_forall_setLIntegral_eq 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace MeasureTheory.lintegral MeasureTheory.Measure.restrict	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ENNReal.aefinStronglyMeasurable_of_aemeasurable ENNReal.instT2Space MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ MeasureTheory.instSigmaFiniteRestrictUnionSet MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict AEMeasurable.restrict MeasureTheory.Measure.restrict_restrict MeasurableSet.inter MeasurableSet.union MeasureTheory.AEFinStronglyMeasurable.measurableSet MeasureTheory.Measure.restrict_apply MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl MeasureTheory.ae.congr_simp Set.compl_union MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl MeasureTheory.ae_restrict_iff' MeasurableSet.compl Filter.mp_mem Filter.EventuallyEq.eq_1 Filter.univ_mem' Set.inter_subset_left Set.inter_subset_right

---

← Back to Index