Documentation Verification Report

IntegralCharFun

📁 Source: Mathlib/MeasureTheory/Measure/IntegralCharFun.lean

Statistics

Metric	Count
Definitions	0
Theorems `integral_charFun_Icc`, `measureReal_abs_dual_gt_le_integral_charFunDual`, `measureReal_abs_gt_le_integral_charFun`, `measureReal_abs_inner_gt_le_integral_charFun`	4
Total	4

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_charFun_Icc` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`intervalIntegral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Real.instNeg` `MeasureSpace.volume` `Real.measureSpace` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `integral` `Real.normedAddCommGroup` `Real.sinc` `Real.instMul`	—	`Set.uIoc_of_le` `Real.instIsOrderedAddMonoid` `LT.lt.le` `integrable_norm_iff` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_mul` `AEStronglyMeasurable.prodMk` `Complex.continuous_ofReal` `AEStronglyMeasurable.fst` `aestronglyMeasurable_id` `TopologicalSpace.pseudoMetrizableSpace_prod` `PseudoEMetricSpace.pseudoMetrizableSpace` `Prod.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `TopologicalSpace.instSecondCountableTopologyProd` `AEStronglyMeasurable.snd` `Nat.cast_one` `Complex.norm_exp_ofReal_mul_I` `integrable_const` `Measure.prod.instIsFiniteMeasure` `Real.isFiniteMeasure_restrict_Ioc` `Nat.instAtLeastTwoHAddOfNat` `charFun_apply_real` `intervalIntegral_integral_swap` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Measure.Regular.toIsFiniteMeasureOnCompacts` `Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `Real.instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Complex.exp_zero` `intervalIntegral.integral_const` `Complex.instCompleteSpace` `sub_neg_eq_add` `Complex.ofReal_add` `mul_one` `two_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `Complex.ofReal_inv` `intervalIntegral.integral_comp_smul_deriv` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `instIsTopologicalRingReal` `HasDerivAt.congr_simp` `mul_comm` `hasDerivAt_mul_const` `continuousOn_const` `Continuous.comp'` `Continuous.fun_mul` `continuous_const` `Complex.ofReal_mul` `intervalIntegral.integral_const_mul` `mul_neg` `mul_assoc` `mul_inv_cancel₀` `one_mul` `integral_exp_mul_I_eq_sinc` `Real.sinc_zero` `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.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `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.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `integral_complex_ofReal` `integral_const_mul`
`measureReal_abs_dual_gt_le_integral_charFunDual` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Measure.real` `setOf` `abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instMul` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Norm.norm` `Complex` `Complex.instNorm` `intervalIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `Complex.instSub` `Complex.instOne` `charFunDual` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instNeg` `MeasureSpace.volume` `Real.measureSpace`	—	`Measure.isProbabilityMeasure_map` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `Real.borelSpace` `Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `map_measureReal_apply` `MeasurableSet.preimage` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.measurable` `Continuous.abs` `instOrderTopologyReal` `continuous_id'` `charFun_map_eq_charFunDual_smul` `measureReal_abs_gt_le_integral_charFun`
`measureReal_abs_gt_le_integral_charFun` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Measure.real` `Real.measurableSpace` `setOf` `abs` `Real.lattice` `Real.instAddGroup` `Real.instMul` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Norm.norm` `Complex` `Complex.instNorm` `intervalIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instSub` `Complex.instOne` `charFun` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Real.instNeg` `MeasureSpace.volume` `Real.measureSpace`	—	`integrable_map_measure` `StronglyMeasurable.aestronglyMeasurable` `Real.stronglyMeasurable_sinc` `AEMeasurable.const_mul` `ContinuousMul.measurableMul` `Real.borelSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `aemeasurable_id` `Real.integrable_sinc` `Measure.isFiniteMeasure_map` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Nat.instAtLeastTwoHAddOfNat` `Set.ext` `abs_mul` `Real.instIsOrderedRing` `Nat.abs_ofNat` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_assoc` `inv_mul_lt_iff₀` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `inv_mul_cancel₀` `ne_of_gt` `lt_inv_mul_iff₀` `mul_one` `abs_inv` `integral_const` `Real.instCompleteSpace` `measureReal_restrict_apply` `Set.univ_inter` `integral_const_mul` `mul_inv_cancel₀` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `setIntegral_mono_on` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Integrable.integrableOn` `integrable_const` `Integrable.sub` `MeasurableSet.preimage` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `instClosedIicTopology` `Measurable.fun_comp` `Continuous.measurable` `Continuous.abs` `instOrderTopologyReal` `continuous_id'` `Measurable.const_mul` `measurable_id'` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.neg_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `abs_zero` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `le_sub_iff_add_le'` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `one_div` `LE.le.trans` `Real.sinc_le_inv_abs` `inv_le_inv₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Meta.Positivity.abs_pos_of_ne_zero` `le_imp_le_of_le_of_le` `setIntegral_le_integral` `Integrable.sub'` `ae_of_all` `Measure.instOuterMeasureClass` `Real.sinc_le_one` `le_refl` `Real.le_norm_self` `Complex.norm_real` `two_mul` `mul_sub` `norm_mul` `NormedDivisionRing.toNormMulClass` `Real.norm_ofNat` `mul_one_sub` `Real.norm_of_nonneg` `mul_pos` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `one_mul` `integral_sub` `probReal_univ` `intervalIntegral.integral_sub` `intervalIntegrable_const` `Real.locallyFinite_volume` `enorm_ne_top` `intervalIntegrable_charFun` `neg_mul` `integral_charFun_Icc` `Complex.ofReal_inv` `intervalIntegral.integral_const` `Complex.instCompleteSpace` `sub_neg_eq_add` `Complex.ofReal_add` `Complex.ofReal_mul`
`measureReal_abs_inner_gt_le_integral_charFun` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Measure.real` `setOf` `abs` `Real.lattice` `Real.instAddGroup` `Inner.inner` `InnerProductSpace.toInner` `Real.instRCLike` `Real.instMul` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Norm.norm` `Complex` `Complex.instNorm` `intervalIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instSub` `Complex.instOne` `charFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.instNeg` `MeasureSpace.volume` `Real.measureSpace`	—	`Measure.isProbabilityMeasure_map` `Continuous.aemeasurable` `Real.borelSpace` `Continuous.inner` `continuous_const` `continuous_id'` `Nat.instAtLeastTwoHAddOfNat` `map_measureReal_apply` `Continuous.measurable` `MeasurableSet.preimage` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.abs` `instOrderTopologyReal` `inner_smul_right` `Complex.ofReal_mul` `conj_trivial` `instTrivialStarReal` `integral_map` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `AEStronglyMeasurable.const_mul` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.continuous_ofReal` `real_inner_comm` `measureReal_abs_gt_le_integral_charFun`

---

← Back to Index