SubGaussian

📁 Source: Mathlib/Probability/Moments/SubGaussian.lean

Statistics

Metric	Count
Definitions `HasCondSubgaussianMGF`, `HasSubgaussianMGF`, `HasSubgaussianMGF`	3
Theorems `ae_condExp_le`, `ae_trim_condExp_le`, `cgf_le`, `fun_zero`, `integrable_exp_mul`, `memLp_exp_mul`, `mgf_le`, `zero`, `add`, `add_of_hasCondSubgaussianMGF`, `add_of_indepFun`, `ae_eq_zero_of_hasSubgaussianMGF_zero`, `aemeasurable`, `aestronglyMeasurable`, `cgf_le`, `congr_identDistrib`, `const_mul`, `fun_zero`, `id_map_iff`, `integrable`, `integrableExpSet_eq_univ`, `integrable_exp_mul`, `measureReal_le_le_exp`, `measure_ge_le`, `measure_sum_ge_le_of_iIndepFun`, `measure_sum_range_ge_le_of_iIndepFun`, `memLp`, `memLp_exp_mul`, `mgf_le`, `neg`, `of_map`, `sub_of_indepFun`, `sum_of_hasCondSubgaussianMGF`, `sum_of_iIndepFun`, `trim`, `zero`, `HasSubgaussianMGF_add_of_HasCondSubgaussianMGF`, `HasSubgaussianMGF_iff_kernel`, `HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF`, `add`, `add_comp`, `add_compProd`, `ae_aestronglyMeasurable`, `ae_eq_zero_of_hasSubgaussianMGF_zero`, `ae_eq_zero_of_hasSubgaussianMGF_zero'`, `ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable`, `ae_forall_integrable_exp_mul`, `ae_forall_memLp_exp_mul`, `ae_integrable_exp_mul`, `aestronglyMeasurable`, `cgf_le`, `const_mul`, `fun_zero`, `id_map_iff`, `integrable_exp_add_compProd`, `integrable_exp_mul`, `isFiniteMeasure`, `measure_ge_le`, `measure_ge_le_exp_add`, `measure_pos_eq_zero_of_hasSubGaussianMGF_zero`, `measure_univ_le_one`, `memLp_exp_mul`, `mgf_le`, `neg`, `of_map`, `of_rat`, `prodMkLeft_compProd`, `zero`, `zero_kernel`, `zero_measure`, `HasSubgaussianMGF_congr`, `hasSubgaussianMGF_of_mem_Icc`, `hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero`, `measure_sum_ge_le_of_HasCondSubgaussianMGF`, `measure_sum_ge_le_of_hasCondSubgaussianMGF`, `mgf_le_of_mem_Icc_of_integral_eq_zero`	76
Total	79

ProbabilityTheory

Definitions

Name	Category	Theorems
`HasCondSubgaussianMGF` 📖	MathDef	2 math math: `HasCondSubgaussianMGF.zero`, `HasCondSubgaussianMGF.fun_zero`
`HasSubgaussianMGF` 📖	CompData	6 math math: `HasSubgaussianMGF_iff_kernel`, `HasSubgaussianMGF.fun_zero`, `hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero`, `HasSubgaussianMGF.id_map_iff`, `HasSubgaussianMGF.zero`, `hasSubgaussianMGF_of_mem_Icc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HasSubgaussianMGF_add_of_HasCondSubgaussianMGF` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `HasSubgaussianMGF` `MeasureTheory.Measure.trim` `HasCondSubgaussianMGF`	`Pi.instAdd` `Real` `Real.instAdd` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`HasSubgaussianMGF.add_of_hasCondSubgaussianMGF`
`HasSubgaussianMGF_iff_kernel` 📖	mathematical	—	`HasSubgaussianMGF` `Kernel.HasSubgaussianMGF` `PUnit.instMeasurableSpace` `Kernel.const` `MeasureTheory.Measure.dirac`	—	`Nat.instAtLeastTwoHAddOfNat` `IsScalarTower.right` `MeasureTheory.Measure.const_comp` `MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `one_smul` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_dirac_eq` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.Countable.to_separableSpace` `instCountablePUnit` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace`
`HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasSubgaussianMGF` `HasCondSubgaussianMGF` `MeasureTheory.Filtration.seq` `MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF`
`hasSubgaussianMGF_of_mem_Icc` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`HasSubgaussianMGF` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `NNReal.instDiv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `sub_sub_sub_cancel_right` `hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero` `AEMeasurable.sub_const` `ContinuousSub.measurableSub` `Real.borelSpace` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Filter.mp_mem` `Filter.univ_mem'` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_add_cancel` `MeasureTheory.integral_sub` `MeasureTheory.Integrable.of_mem_Icc` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.integrable_const` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.probReal_univ` `one_mul` `sub_self`
`hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instZero`	`HasSubgaussianMGF` `NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `NNReal.instDiv` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instSub` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `integrable_exp_mul_of_mem_Icc` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `lt_trichotomy` `mgf_le_of_mem_Icc_of_integral_eq_zero` `mgf_zero'` `MeasureTheory.probReal_univ` `zero_pow` `Nat.instCharZero` `MulZeroClass.mul_zero` `zero_div` `Real.exp_zero` `mul_neg` `neg_mul` `neg_neg` `AEMeasurable.neg` `ContinuousNeg.measurableNeg` `Real.borelSpace` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `Filter.mp_mem` `Filter.univ_mem'` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `MeasureTheory.integral_neg` `neg_zero` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `mul_one` `add_zero` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.isInt_pow` `Mathlib.Meta.NormNum.intPow_negOfNat_bit0` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Tactic.RingNF.nnrat_rawCast` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.one_pow`
`measure_sum_ge_le_of_HasCondSubgaussianMGF` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasSubgaussianMGF` `HasCondSubgaussianMGF` `MeasureTheory.Filtration.seq` `MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `Real.instLE` `Real.instZero`	`MeasureTheory.Measure.real` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`measure_sum_ge_le_of_hasCondSubgaussianMGF`
`measure_sum_ge_le_of_hasCondSubgaussianMGF` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasSubgaussianMGF` `HasCondSubgaussianMGF` `MeasureTheory.Filtration.seq` `MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `Real.instLE` `Real.instZero`	`MeasureTheory.Measure.real` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `HasSubgaussianMGF.measure_ge_le` `HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF`
`mgf_le_of_mem_Icc_of_integral_eq_zero` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `Filter.Eventually` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instZero` `Real.instLT`	`Real.instLE` `mgf` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `NNReal.toReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `integrable_exp_mul_of_mem_Icc` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `interior_univ` `Nat.instAtLeastTwoHAddOfNat` `exists_cgf_eq_iteratedDeriv_two_cgf_mul` `exp_cgf` `MeasureTheory.IsProbabilityMeasure.neZero` `Real.exp_le_exp` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `variance_tilted_mul` `Set.mem_Icc_of_Ioo` `variance_le_sq_of_bounded` `MeasureTheory.isProbabilityMeasure_tilted` `MeasureTheory.tilted_absolutelyContinuous` `AEMeasurable.mono_ac` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `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.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `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` `sq_abs` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial`

ProbabilityTheory.HasCondSubgaussianMGF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_condExp_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`Filter.Eventually` `Real` `Real.instLE` `MeasureTheory.condExp` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.exp` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NNReal.toReal` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.ae_of_ae_trim` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `ae_trim_condExp_le`
`ae_trim_condExp_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`Filter.Eventually` `Real` `Real.instLE` `MeasureTheory.condExp` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.exp` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NNReal.toReal` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Real.instCompleteSpace` `MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel` `MeasureTheory.isFiniteMeasure_trim` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.instIsMarkovKernelCondExpKernel` `ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel` `ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul` `Filter.mp_mem` `ProbabilityTheory.condExpKernel_comp_trim` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.ae.congr_simp` `MeasureTheory.Measure.trim.congr_simp` `ProbabilityTheory.condExpKernel.congr_simp` `mgf_le` `Filter.univ_mem'`
`cgf_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le`
`fun_zero` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`ProbabilityTheory.HasCondSubgaussianMGF` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero` `MeasureTheory.isFiniteMeasure_trim` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.instIsMarkovKernelCondExpKernel`
`integrable_exp_mul` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul` `ProbabilityTheory.condExpKernel_comp_trim`
`memLp_exp_mul` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `Real.exp` `Real.instMul` `ENNReal.ofNNReal`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul` `ProbabilityTheory.condExpKernel_comp_trim`
`mgf_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasCondSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le`
`zero` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`ProbabilityTheory.HasCondSubgaussianMGF` `Pi.instZero` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.zero` `MeasureTheory.isFiniteMeasure_trim` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.instIsMarkovKernelCondExpKernel`

ProbabilityTheory.HasSubgaussianMGF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`Real` `Real.instAdd` `NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.add` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`add_of_hasCondSubgaussianMGF` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `ProbabilityTheory.HasSubgaussianMGF` `MeasureTheory.Measure.trim` `ProbabilityTheory.HasCondSubgaussianMGF`	`Pi.instAdd` `Real` `Real.instAdd` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`ProbabilityTheory.HasSubgaussianMGF_iff_kernel` `IsScalarTower.right` `MeasureTheory.Measure.const_comp` `MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `one_smul` `ProbabilityTheory.Kernel.ext` `ProbabilityTheory.Kernel.const_apply` `MeasureTheory.Measure.compProd.eq_1` `ProbabilityTheory.compProd_trim_condExpKernel` `ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp` `MeasureTheory.instSFiniteOfCountable` `instCountablePUnit` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.instIsMarkovKernelCondExpKernel` `of_map` `Measurable.aemeasurable` `Measurable.prodMk` `measurable_id''` `measurable_id`
`add_of_indepFun` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF` `ProbabilityTheory.IndepFun` `Real` `Real.measurableSpace`	`Real.instAdd` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`mul_add` `Distrib.leftDistribClass` `Real.exp_add` `MeasureTheory.MemLp.integrable_mul` `Nat.instAtLeastTwoHAddOfNat` `memLp_exp_mul` `Nat.cast_one` `ENNReal.HolderConjugate.instTwoTwo` `ProbabilityTheory.IndepFun.mgf_add` `integrable_exp_mul` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mgf_le` `ProbabilityTheory.mgf_nonneg` `le_of_lt` `Real.exp_pos` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`
`ae_eq_zero_of_hasSubgaussianMGF_zero` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF` `NNReal` `instZeroNNReal`	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `Real.instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_dirac_eq` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.Countable.to_separableSpace` `instCountablePUnit` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`aemeasurable` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`AEMeasurable` `Real` `Real.measurableSpace`	—	`MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `aestronglyMeasurable`
`aestronglyMeasurable` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`integrable_exp_mul` `one_mul` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Real.aemeasurable_of_aemeasurable_exp` `MeasureTheory.AEStronglyMeasurable.aemeasurable`
`cgf_le` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`Real` `Real.instLE` `ProbabilityTheory.cgf` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `NNReal.toReal` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_dirac_eq` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.Countable.to_separableSpace` `instCountablePUnit` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `MeasureTheory.all_ae_of` `ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`congr_identDistrib` 📖	—	`ProbabilityTheory.HasSubgaussianMGF` `ProbabilityTheory.IdentDistrib` `Real` `Real.measurableSpace`	—	—	`id_map_iff` `ProbabilityTheory.IdentDistrib.aemeasurable_snd` `ProbabilityTheory.IdentDistrib.map_eq` `ProbabilityTheory.IdentDistrib.aemeasurable_fst`
`const_mul` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`Real` `Real.instMul` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real.instLE` `Real.instZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Real.semiring` `sq_nonneg` `Real.linearOrder` `AddGroup.existsAddOfLE` `Real.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsOrderedRing.toPosMulMono` `Real.partialOrder` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instAddCommMonoid` `Real.instIsOrderedAddMonoid`	—	`sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel` `ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul`
`fun_zero` 📖	mathematical	—	`ProbabilityTheory.HasSubgaussianMGF` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`MeasureTheory.Measure.dirac.instIsFiniteMeasure` `ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel`
`id_map_iff` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`ProbabilityTheory.HasSubgaussianMGF` `MeasureTheory.Measure.map`	—	`of_map` `MeasureTheory.integrable_map_measure` `Continuous.comp_aestronglyMeasurable` `Continuous.rexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `integrable_exp_mul` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityTheory.mgf_id_map` `mgf_le`
`integrable` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`ProbabilityTheory.integrable_of_mem_interior_integrableExpSet` `integrableExpSet_eq_univ` `interior_univ`
`integrableExpSet_eq_univ` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`ProbabilityTheory.integrableExpSet` `Set.univ` `Real`	—	`Set.ext` `integrable_exp_mul`
`integrable_exp_mul` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul`	—	—
`measureReal_le_le_exp` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF` `Real` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `ProbabilityTheory.IndepFun` `Real.measurableSpace` `Real.instLE`	`MeasureTheory.Measure.real` `setOf` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instAdd` `NNReal.toReal`	—	`Nat.instAtLeastTwoHAddOfNat` `LE.le.trans_eq` `measure_ge_le` `add_comm` `sub_of_indepFun` `ProbabilityTheory.IndepFun.comp` `ProbabilityTheory.IndepFun.symm` `Measurable.sub_const` `ContinuousSub.measurableSub` `Real.borelSpace` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `measurable_id'`
`measure_ge_le` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF` `Real` `Real.instLE` `Real.instZero`	`MeasureTheory.Measure.real` `setOf` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_dirac_eq` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.Countable.to_separableSpace` `instCountablePUnit` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`measure_sum_ge_le_of_iIndepFun` 📖	mathematical	`ProbabilityTheory.iIndepFun` `Real` `Real.measurableSpace` `ProbabilityTheory.HasSubgaussianMGF` `Real.instLE` `Real.instZero`	`MeasureTheory.Measure.real` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`measure_ge_le` `sum_of_iIndepFun`
`measure_sum_range_ge_le_of_iIndepFun` 📖	mathematical	`ProbabilityTheory.iIndepFun` `Real` `Real.measurableSpace` `ProbabilityTheory.HasSubgaussianMGF` `Real.instLE` `Real.instZero`	`MeasureTheory.Measure.real` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal`	—	`Nat.instAtLeastTwoHAddOfNat` `measure_ge_le` `sum_of_iIndepFun` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `NNReal.coe_natCast`
`memLp` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `ENNReal.ofNNReal`	—	`ProbabilityTheory.memLp_of_mem_interior_integrableExpSet` `integrableExpSet_eq_univ` `interior_univ`
`memLp_exp_mul` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `Real.exp` `Real.instMul` `ENNReal.ofNNReal`	—	`IsScalarTower.right` `MeasureTheory.Measure.const_comp` `MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `one_smul` `ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`mgf_le` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`Real` `Real.instLE` `ProbabilityTheory.mgf` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `NNReal.toReal` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	—
`neg` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF`	`Pi.instNeg` `Real` `Real.instNeg`	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF.neg` `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`
`of_map` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.HasSubgaussianMGF` `MeasureTheory.Measure.map`	`Real`	—	`integrable_exp_mul` `MeasureTheory.integrable_map_measure` `MeasureTheory.Integrable.aestronglyMeasurable` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityTheory.mgf_map` `mgf_le`
`sub_of_indepFun` 📖	mathematical	`ProbabilityTheory.HasSubgaussianMGF` `ProbabilityTheory.IndepFun` `Real` `Real.measurableSpace`	`Real.instSub` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`sub_eq_add_neg` `add_of_indepFun` `neg` `ProbabilityTheory.IndepFun.neg_right` `ContinuousNeg.measurableNeg` `Real.borelSpace` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal`
`sum_of_hasCondSubgaussianMGF` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ProbabilityTheory.HasSubgaussianMGF` `ProbabilityTheory.HasCondSubgaussianMGF` `MeasureTheory.Filtration.seq` `MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`MeasureTheory.Filtration.le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `Finset.sum_congr` `zero_add` `Finset.sum_singleton` `Finset.sum_range_succ` `add_of_hasCondSubgaussianMGF` `trim` `Finset.measurable_fun_sum` `ContinuousAdd.measurableMul₂` `Real.borelSpace` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.StronglyMeasurable.mono` `MeasureTheory.Filtration.mono`
`sum_of_iIndepFun` 📖	mathematical	`ProbabilityTheory.iIndepFun` `Real` `Real.measurableSpace` `ProbabilityTheory.HasSubgaussianMGF`	`Finset.sum` `Real.instAddCommMonoid` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`ProbabilityTheory.iIndepFun.precomp` `Subtype.val_injective` `aemeasurable` `congr` `Finset.sum_coe_sort` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `Finset.sum_attach`
`trim` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `Measurable` `Real` `Real.measurableSpace` `ProbabilityTheory.HasSubgaussianMGF`	`MeasureTheory.Measure.trim`	—	`MeasureTheory.Integrable.trim` `integrable_exp_mul` `Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Measurable.exp` `Measurable.const_mul` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityTheory.mgf.eq_1` `MeasureTheory.integral_trim` `mgf_le`
`zero` 📖	mathematical	—	`ProbabilityTheory.HasSubgaussianMGF` `Pi.instZero` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`fun_zero`

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
`HasSubgaussianMGF` 📖	CompData	8 math math: `ProbabilityTheory.HasSubgaussianMGF_iff_kernel`, `HasSubgaussianMGF_congr`, `HasSubgaussianMGF.of_rat`, `HasSubgaussianMGF.id_map_iff`, `HasSubgaussianMGF.zero`, `HasSubgaussianMGF.zero_kernel`, `HasSubgaussianMGF.zero_measure`, `HasSubgaussianMGF.fun_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HasSubgaussianMGF_congr` 📖	mathematical	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`HasSubgaussianMGF`	—	`MeasureTheory.Measure.instOuterMeasureClass` `HasSubgaussianMGF.congr` `MeasureTheory.ae_eq_symm`

ProbabilityTheory.Kernel.HasSubgaussianMGF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Real` `Real.instAdd` `NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt`	—	`NNReal.sqrt_zero` `zero_add` `NNReal.sq_sqrt` `congr` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_eq_zero_of_hasSubgaussianMGF_zero'` `Filter.univ_mem'` `add_zero` `mul_add` `Distrib.leftDistribClass` `Real.exp_add` `MeasureTheory.MemLp.integrable_mul` `Nat.instAtLeastTwoHAddOfNat` `memLp_exp_mul` `Nat.cast_one` `ENNReal.HolderConjugate.instTwoTwo` `ae_forall_memLp_exp_mul` `mgf_le` `MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg` `Real.coe_sqrt` `inv_div` `inv_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `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.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sqrt_pos_of_pos` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `NNReal.addLeftMono` `NNReal.sqrt_pos_of_pos` `MeasureTheory.ae_of_all` `Real.exp_nonneg` `ENNReal.ofReal_coe_nnreal` `Real.exp_mul` `mul_right_comm` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Real.rpow_le_rpow` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `le_of_lt` `Real.exp_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Real.rpow_nonneg` `Real.rpow_pos_of_pos` `one_div` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Mathlib.Tactic.LinearCombination.add_eq_eq` `Real.sq_sqrt` `NNReal.coe_nonneg` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `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.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.cast_zero`
`add_comp` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	`Prod.instMeasurableSpace` `Real` `Real.instAdd` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `ProbabilityTheory.Kernel.compProd` `ProbabilityTheory.Kernel.prodMkLeft`	—	`add_compProd` `ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft` `prodMkLeft_compProd`
`add_compProd` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	`Real` `Real.instAdd` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `ProbabilityTheory.Kernel.compProd`	—	`of_rat` `integrable_exp_add_compProd` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.ae_integrable_of_integrable_comp` `MeasureTheory.Measure.ae_ae_of_ae_compProd` `mgf_le` `ae_integrable_exp_mul` `Filter.univ_mem'` `mul_add` `Distrib.leftDistribClass` `Real.exp_add` `ProbabilityTheory.integral_compProd` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `MeasureTheory.integral_const_mul` `MeasureTheory.integral_mono_of_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.ae_of_all` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Real.exp_pos` `MeasureTheory.integral_nonneg` `MeasureTheory.Integrable.mul_const` `MeasureTheory.all_ae_of` `mul_le_mul_of_nonneg_left` `MeasureTheory.integral_mul_const` `NNReal.coe_add` `add_mul` `Distrib.rightDistribClass` `add_div` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left`
`ae_aestronglyMeasurable` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ae_integrable_exp_mul` `Filter.mp_mem` `Filter.univ_mem'` `one_mul` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Real.aemeasurable_of_aemeasurable_exp` `MeasureTheory.AEStronglyMeasurable.aemeasurable`
`ae_eq_zero_of_hasSubgaussianMGF_zero` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `NNReal` `instZeroNNReal`	`Filter.Eventually` `Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Pi.instZero` `Real.instZero`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `measure_pos_eq_zero_of_hasSubGaussianMGF_zero` `neg` `Filter.univ_mem'` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.measure_union_le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_zero`
`ae_eq_zero_of_hasSubgaussianMGF_zero'` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `NNReal` `instZeroNNReal`	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Pi.instZero` `Real.instZero`	—	`aestronglyMeasurable` `congr` `Filter.EventuallyEq.trans` `MeasureTheory.Measure.instOuterMeasureClass` `ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace`
`ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `ProbabilityTheory.Kernel.HasSubgaussianMGF` `NNReal` `instZeroNNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Pi.instZero` `Real.instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.eq_1` `MeasureTheory.Measure.ae_comp_iff` `measurableSet_eq_fun` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `measurable_zero` `ae_eq_zero_of_hasSubgaussianMGF_zero`
`ae_forall_integrable_exp_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ae_integrable_exp_mul` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `instCountableInt` `Filter.univ_mem'` `ProbabilityTheory.integrable_exp_mul_of_le_of_le` `Int.floor_le` `Int.le_ceil`
`ae_forall_memLp_exp_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ae_forall_integrable_exp_mul` `Filter.univ_mem'` `MeasureTheory.eLpNorm_exponent_zero` `MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top` `Nat.cast_zero` `ENNReal.coe_toReal` `MeasureTheory.Integrable.lintegral_lt_top` `Real.enorm_eq_ofReal` `le_of_lt` `Real.exp_pos` `ENNReal.ofReal_rpow_of_nonneg` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Real.exp_mul` `mul_comm` `mul_assoc`
`ae_integrable_exp_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.ae_integrable_of_integrable_comp` `integrable_exp_mul`
`aestronglyMeasurable` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`integrable_exp_mul` `one_mul` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Real.aemeasurable_of_aemeasurable_exp` `MeasureTheory.AEStronglyMeasurable.aemeasurable`
`cgf_le` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `ae_forall_integrable_exp_mul` `mgf_le` `Filter.univ_mem'` `ProbabilityTheory.mgf_zero_measure` `Real.log_zero` `Real.log_exp` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.log_le_log` `ProbabilityTheory.mgf_pos'` `le_refl`
`const_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Real` `Real.instMul` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real.instLE` `Real.instZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Real.semiring` `sq_nonneg` `Real.linearOrder` `AddGroup.existsAddOfLE` `Real.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsOrderedRing.toPosMulMono` `Real.partialOrder` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instAddCommMonoid` `Real.instIsOrderedAddMonoid`	—	`sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `integrable_exp_mul` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `mgf_le` `Filter.univ_mem'` `ProbabilityTheory.mgf_const_mul` `mul_comm` `LE.le.trans_eq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw`
`fun_zero` 📖	mathematical	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`MulZeroClass.mul_zero` `Real.exp_zero` `MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `enorm_one` `NormedDivisionRing.to_normOneClass` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.mgf_const'` `mul_one` `MulZeroClass.zero_mul` `zero_div` `MeasureTheory.ae_of_all` `MeasureTheory.measureReal_le_one` `ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure`
`id_map_iff` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `ProbabilityTheory.Kernel.map`	—	`of_map` `ProbabilityTheory.Kernel.deterministic_comp_eq_map` `MeasureTheory.Measure.comp_assoc` `MeasureTheory.Measure.deterministic_comp_eq_map` `MeasureTheory.integrable_map_measure` `Continuous.comp_aestronglyMeasurable` `Continuous.rexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Measurable.aemeasurable` `integrable_exp_mul` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.Kernel.map_apply` `ProbabilityTheory.mgf_id_map` `mgf_le`
`integrable_exp_add_compProd` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `Real.instAdd` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ProbabilityTheory.Kernel.compProd`	—	`ProbabilityTheory.eq_zero_or_isMarkovKernel` `ProbabilityTheory.Kernel.compProd_zero_right` `MeasureTheory.Measure.bind_zero_right` `mul_add` `Distrib.leftDistribClass` `Real.exp_add` `MeasureTheory.MemLp.integrable_mul` `Nat.instAtLeastTwoHAddOfNat` `memLp_exp_mul` `MeasureTheory.Measure.map_comp` `measurable_fst` `ProbabilityTheory.Kernel.fst_eq` `ProbabilityTheory.Kernel.fst_compProd` `MeasureTheory.memLp_map_measure_iff` `Measurable.aemeasurable` `MeasureTheory.Measure.snd.eq_1` `MeasureTheory.Measure.comp_compProd_comm` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ENNReal.coe_ofNat` `measurable_snd` `ENNReal.HolderConjugate.instTwoTwo` `ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left`
`integrable_exp_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	—
`isFiniteMeasure` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.IsFiniteMeasure` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `mgf_le` `ae_integrable_exp_mul` `Filter.univ_mem'` `MulZeroClass.zero_mul` `Real.exp_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`measure_ge_le` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `Real` `Real.instLE` `Real.instZero`	`Filter.Eventually` `MeasureTheory.Measure.real` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `setOf` `Real.exp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `NNReal.toReal` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `measure_univ_le_one` `Filter.univ_mem'` `MulZeroClass.mul_zero` `div_zero` `Real.exp_zero` `ENNReal.toReal_le_of_le_ofReal` `zero_le_one` `Real.instZeroLEOneClass` `ENNReal.ofReal_one` `LE.le.trans` `MeasureTheory.measure_mono` `Set.subset_univ` `measure_ge_le_exp_add` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `mul_neg` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `neg_div` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `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` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul`
`measure_ge_le_exp_add` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `isFiniteMeasure` `ae_forall_integrable_exp_mul` `mgf_le` `Filter.univ_mem'` `ProbabilityTheory.measure_ge_le_exp_mul_mgf` `Real.exp_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Real.exp_pos`
`measure_pos_eq_zero_of_hasSubGaussianMGF_zero` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `NNReal` `instZeroNNReal`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `setOf` `Real` `Real.instLT` `Real.instZero` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Set.ext` `exists_rat_btwn` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Rat.cast_pos` `LT.lt.le` `lt_of_lt_of_le` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `isFiniteMeasure` `Nat.instAtLeastTwoHAddOfNat` `measure_ge_le_exp_add` `Filter.univ_mem'` `Filter.Tendsto.comp` `Real.tendsto_exp_neg_atTop_nhds_zero` `Filter.Tendsto.atTop_mul_const` `le_antisymm` `ge_of_tendsto` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Filter.eventually_atTop` `neg_mul` `MulZeroClass.zero_mul` `zero_div` `add_zero` `MeasureTheory.measureReal_nonneg` `MeasureTheory.ae_all_iff` `Encodable.countable` `Subtype.countable`
`measure_univ_le_one` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `mgf_le` `isFiniteMeasure` `Filter.univ_mem'` `MulZeroClass.zero_mul` `Real.exp_zero` `MeasureTheory.integral_const` `Real.instCompleteSpace` `mul_one` `zero_pow` `Nat.instCharZero` `MulZeroClass.mul_zero` `zero_div` `ENNReal.ofReal_one` `ENNReal.le_ofReal_iff_toReal_le` `MeasureTheory.measure_ne_top` `zero_le_one` `Real.instZeroLEOneClass`
`memLp_exp_mul` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `Real.exp` `Real.instMul` `ENNReal.ofNNReal` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`integrable_exp_mul` `MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top` `Nat.cast_zero` `Real.enorm_eq_ofReal` `le_of_lt` `Real.exp_pos` `ENNReal.ofReal_rpow_of_nonneg` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Real.exp_mul` `mul_comm` `mul_assoc` `MeasureTheory.hasFiniteIntegral_def`
`mgf_le` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—
`neg` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	`Pi.instNeg` `Real` `Real.instNeg`	—	`mul_neg` `neg_mul` `integrable_exp_mul` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `mgf_le` `Filter.univ_mem'` `Even.neg_pow`
`of_map` 📖	mathematical	`Measurable` `ProbabilityTheory.Kernel.HasSubgaussianMGF` `ProbabilityTheory.Kernel.map`	`Real`	—	`integrable_exp_mul` `MeasureTheory.integrable_map_measure` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.Measure.map_comp` `Measurable.aemeasurable` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `mgf_le` `ae_forall_integrable_exp_mul` `Filter.univ_mem'` `ProbabilityTheory.Kernel.map_apply` `ProbabilityTheory.mgf_map`
`of_rat` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `Filter.Eventually` `Real.instLE` `ProbabilityTheory.mgf` `Real.instRatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NNReal.toReal` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`ProbabilityTheory.Kernel.HasSubgaussianMGF`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.ae_integrable_of_integrable_comp` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `instCountableInt` `Filter.univ_mem'` `ProbabilityTheory.integrable_exp_mul_of_le_of_le` `Int.floor_le` `Int.le_ceil` `Encodable.countable` `DenseRange.induction_on` `Rat.denseRange_cast` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Real.instArchimedean` `isClosed_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ProbabilityTheory.continuous_mgf` `Continuous.rexp` `Continuous.comp'` `Continuous.div_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id'` `Continuous.fun_mul` `continuous_const` `Continuous.pow`
`prodMkLeft_compProd` 📖	mathematical	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `MeasureTheory.Measure.bind` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	`Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.prodMkLeft` `MeasureTheory.Measure.compProd`	—	`MeasureTheory.Measure.prodMkLeft_comp_compProd` `integrable_exp_mul` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `mgf_le` `MeasureTheory.ae_of_ae_map` `AEMeasurable.snd` `aemeasurable_id` `MeasureTheory.Measure.snd.eq_1` `MeasureTheory.Measure.snd_compProd` `MeasureTheory.Measure.compProd_of_not_isSFiniteKernel` `MeasureTheory.Measure.compProd_of_not_sfinite`
`zero` 📖	mathematical	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `Pi.instZero` `Real` `Real.instZero` `NNReal` `instZeroNNReal`	—	`fun_zero`
`zero_kernel` 📖	mathematical	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instZero`	—	`MeasureTheory.Measure.bind_zero_right` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.mgf_zero_measure`
`zero_measure` 📖	mathematical	—	`ProbabilityTheory.Kernel.HasSubgaussianMGF` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasureTheory.Measure.bind_zero_left` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_zero`

---

← Back to Index