VitaliCaratheodory

📁 Source: Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_le_lowerSemicontinuous_lintegral_ge, exists_upperSemicontinuous_le_lintegral_le, exists_le_lowerSemicontinuous_lintegral_ge, exists_lt_lowerSemicontinuous_integral_gt_nnreal, exists_lt_lowerSemicontinuous_integral_lt, exists_lt_lowerSemicontinuous_lintegral_ge, exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable, exists_upperSemicontinuous_le_integral_le, exists_upperSemicontinuous_le_lintegral_le, exists_upperSemicontinuous_lt_integral_gt	10
Total	10

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_lowerSemicontinuous_lintegral_ge 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder LowerSemicontinuous lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	ENNReal.exists_pos_sum_of_countable' instCountableNat SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge LT.lt.ne' SimpleFunc.tsum_eapproxDiff ENNReal.tsum_le_tsum ENNReal.coe_le_coe lowerSemicontinuous_tsum Continuous.comp_lowerSemicontinuous NNReal.instOrderTopology ENNReal.instOrderTopology ENNReal.continuous_coe lintegral_tsum Measurable.aemeasurable Measurable.coe_nnreal_ennreal LowerSemicontinuous.measurable NNReal.borelSpace NNReal.instSecondCountableTopology BorelSpace.opensMeasurable ENNReal.tsum_add add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add SimpleFunc.measurable LT.lt.le
exists_lt_lowerSemicontinuous_integral_gt_nnreal 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NNReal.toReal Real.instLT Real.instZero	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal LowerSemicontinuous Filter.Eventually Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal.toReal integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instAdd	—	Real.toNNReal_coe AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace NNReal.borelSpace AEStronglyMeasurable.real_toNNReal Integrable.aestronglyMeasurable Measure.instOuterMeasureClass CanLift.prf NNReal.canLift LT.lt.le exists_between NNReal.instDenselyOrdered LT.lt.ne hasFiniteIntegral_iff_ofNNReal Integrable.hasFiniteIntegral exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable ENNReal.coe_ne_zero LT.lt.ne' ne_top_of_le_ne_top ae_lt_top LowerSemicontinuous.measurable ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable lintegral_congr_ae Filter.mp_mem Filter.univ_mem' ENNReal.ofReal_toReal AEMeasurable.aestronglyMeasurable Real.borelSpace instSecondCountableTopologyReal Measurable.aemeasurable Measurable.ennreal_toReal abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.toReal_nonneg Ne.lt_top integral_eq_lintegral_of_nonneg_ae Filter.Eventually.of_forall AEMeasurable.coe_nnreal_real ENNReal.toReal_mono ENNReal.toReal_add ENNReal.coe_ne_top ENNReal.coe_toReal add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd ENNReal.ofReal_coe_nnreal
exists_lt_lowerSemicontinuous_integral_lt 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instLT Real.instZero	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal LowerSemicontinuous EReal.toReal Filter.Eventually Top.top EReal.instTop ae Measure Measure.instFunLike Measure.instOuterMeasureClass integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat LT.lt.le half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Integrable.real_toNNReal Measure.instOuterMeasureClass exists_lt_lowerSemicontinuous_integral_gt_nnreal Integrable.neg exists_upperSemicontinuous_le_integral_le Filter.mp_mem Filter.univ_mem' EReal.toReal_sub LT.lt.ne EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal EReal.sub_lt_sub_of_lt_of_le LowerSemicontinuous.add' instIsOrderedAddMonoidEReal EReal.instOrderTopology Continuous.comp_lowerSemicontinuous ENNReal.instOrderTopology continuous_coe_ennreal_ereal EReal.coe_ennreal_le_coe_ennreal_iff Continuous.comp_upperSemicontinuous_antitone ContinuousNeg.continuous_neg EReal.instContinuousNeg Continuous.comp_upperSemicontinuous NNReal.instOrderTopology ENNReal.continuous_coe ENNReal.coe_le_coe EReal.neg_le_neg_iff EReal.continuousAt_add integrable_congr EReal.toReal_coe_ennreal Integrable.sub sub_eq_add_neg EReal.add_lt_top lt_top_iff_ne_top integral_congr_ae integral_sub sub_lt_sub_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_le_sub_left integral_eq_integral_pos_part_sub_integral_neg_part Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial
exists_lt_lowerSemicontinuous_lintegral_ge 📖	mathematical	Measurable NNReal NNReal.measurableSpace	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal LowerSemicontinuous Preorder.toLE lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' ENNReal.half_pos exists_pos_lintegral_lt_of_sigmaFinite exists_le_lowerSemicontinuous_lintegral_ge Measurable.coe_nnreal_ennreal Measurable.add ContinuousAdd.measurableMul₂ NNReal.borelSpace NNReal.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring add_zero add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftMono lintegral_add_right le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid add_le_add_right le_of_lt le_refl add_assoc ENNReal.add_halves
exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal LowerSemicontinuous Preorder.toLE lintegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' ENNReal.half_pos exists_lt_lowerSemicontinuous_lintegral_ge exists_measurable_superset_of_null exists_le_lowerSemicontinuous_lintegral_ge Measurable.indicator measurable_const Set.indicator_of_mem add_top Set.compl_subset_comm LT.lt.trans_le le_self_add ENNReal.instCanonicallyOrderedAdd LowerSemicontinuous.add ENNReal.instIsOrderedAddMonoid ENNReal.instOrderTopology ENNReal.instContinuousAdd lintegral_add_left LowerSemicontinuous.measurable ENNReal.borelSpace ENNReal.instSecondCountableTopology BorelSpace.opensMeasurable add_le_add IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add lintegral_congr_ae Filter.EventuallyEq.fun_comp Measure.instOuterMeasureClass lintegral_indicator lintegral_const Measure.restrict_apply Set.univ_inter MulZeroClass.mul_zero zero_add add_assoc ENNReal.add_halves
exists_upperSemicontinuous_le_integral_le 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NNReal.toReal Real.instLT Real.instZero	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal UpperSemicontinuous Real.instLE Real.instSub integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	CanLift.prf NNReal.canLift LT.lt.le hasFiniteIntegral_iff_ofNNReal Integrable.hasFiniteIntegral exists_upperSemicontinuous_le_lintegral_le LT.lt.ne LT.lt.ne' ENNReal.coe_pos NNReal.coe_pos lt_of_le_of_lt lintegral_mono Integrable.mono AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal Measurable.aemeasurable Measurable.coe_nnreal_real UpperSemicontinuous.measurable NNReal.borelSpace NNReal.instOrderTopology NNReal.instSecondCountableTopology Filter.Eventually.of_forall Measure.instOuterMeasureClass NNReal.abs_eq integral_eq_lintegral_of_nonneg_ae Integrable.aestronglyMeasurable sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_coe_nnreal ENNReal.toReal_add ENNReal.coe_ne_top ENNReal.toReal_mono
exists_upperSemicontinuous_le_lintegral_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal UpperSemicontinuous ENNReal ENNReal.instPartialOrder lintegral ENNReal.ofNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Nat.instAtLeastTwoHAddOfNat ENNReal.lt_add_right LT.lt.ne' ENNReal.half_pos ENNReal.biSup_add ENNReal.instCanonicallyOrderedAdd lintegral_eq_nnreal SimpleFunc.lintegral_eq_lintegral LT.lt.le ne_top_of_le_ne_top lintegral_mono SimpleFunc.exists_upperSemicontinuous_le_lintegral_le LE.le.trans add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_rfl add_assoc ENNReal.add_halves
exists_upperSemicontinuous_lt_integral_gt 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instLT Real.instZero	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal UpperSemicontinuous EReal.toReal Filter.Eventually Bot.bot instBotEReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instAdd	—	Measure.instOuterMeasureClass exists_lt_lowerSemicontinuous_integral_lt Integrable.neg EReal.neg_lt_comm Continuous.comp_lowerSemicontinuous_antitone EReal.instOrderTopology ContinuousNeg.continuous_neg EReal.instContinuousNeg EReal.neg_le_neg_iff EReal.toReal_neg_eq integral_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_comm

MeasureTheory.SimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_lowerSemicontinuous_lintegral_ge 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe MeasureTheory.SimpleFunc instFunLike LowerSemicontinuous ENNReal ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	induction Set.piecewise_eq_indicator Set.indicator_le_self NNReal.instCanonicallyOrderedAdd lowerSemicontinuous_const top_add piecewise.congr_simp Set.indicator_zero' MeasureTheory.lintegral_const MulZeroClass.zero_mul ENNReal.instCanonicallyOrderedAdd ENNReal.coe_indicator MeasureTheory.lintegral_indicator MeasureTheory.Measure.restrict_apply Set.univ_inter ENNReal.div_pos_iff ENNReal.coe_ne_top add_zero ENNReal.add_lt_add_left Set.exists_isOpen_lt_of_lt MeasureTheory.Measure.WeaklyRegular.toOuterRegular le_imp_le_of_le_of_le le_refl Set.indicator_le_indicator_apply_of_subset le_of_lt lt_of_le_of_ne' zero_le IsOpen.lowerSemicontinuous_indicator mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid mul_add Distrib.leftDistribClass ENNReal.mul_div_cancel IsOpen.measurableSet BorelSpace.opensMeasurable Nat.instAtLeastTwoHAddOfNat LT.lt.ne' ENNReal.half_pos add_le_add NNReal.addLeftMono covariant_swap_add_of_covariant_add LowerSemicontinuous.add IsOrderedRing.toIsOrderedAddMonoid NNReal.instIsOrderedRing NNReal.instOrderTopology IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring MeasureTheory.lintegral_add_left Measurable.coe_nnreal_ennreal measurable LowerSemicontinuous.measurable NNReal.borelSpace NNReal.instSecondCountableTopology ENNReal.add_halves Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.term_add_term Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_term IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid
exists_upperSemicontinuous_le_lintegral_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe MeasureTheory.SimpleFunc instFunLike UpperSemicontinuous ENNReal ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	induction piecewise.congr_simp piecewise_same MeasureTheory.lintegral_const MulZeroClass.zero_mul zero_add ENNReal.instCanonicallyOrderedAdd Set.piecewise_eq_indicator ENNReal.coe_indicator MeasureTheory.lintegral_indicator MeasureTheory.Measure.restrict_apply Set.univ_inter ENNReal.div_pos_iff ENNReal.coe_ne_top MeasurableSet.exists_isClosed_lt_add LT.lt.ne LT.lt.ne' le_imp_le_of_le_of_le Set.indicator_le_indicator_apply_of_subset le_of_lt lt_of_le_of_ne' zero_le NNReal.instCanonicallyOrderedAdd le_refl IsClosed.upperSemicontinuous_indicator mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid mul_add Distrib.leftDistribClass ENNReal.mul_div_cancel IsClosed.measurableSet BorelSpace.opensMeasurable MeasureTheory.lintegral_add_left Measurable.coe_nnreal_ennreal measurable Nat.instAtLeastTwoHAddOfNat ENNReal.add_ne_top ENNReal.half_pos add_le_add NNReal.addLeftMono covariant_swap_add_of_covariant_add UpperSemicontinuous.add IsOrderedRing.toIsOrderedAddMonoid NNReal.instIsOrderedRing NNReal.instOrderTopology IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring UpperSemicontinuous.measurable NNReal.borelSpace NNReal.instSecondCountableTopology ENNReal.add_halves Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const Mathlib.Tactic.Abel.term_add_term Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_term IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid

---

← Back to Index