Fernique

📁 Source: Mathlib/Probability/Distributions/Fernique.lean

Statistics

Metric	Count
Definitions rotation, logRatio, normThreshold	3
Theorems rotation_apply, lintegral_closedBall_diff_exp_logRatio_mul_sq_le, lintegral_exp_mul_sq_norm_le_mul, logRatio_mono, logRatio_mul_normThreshold_add_one_le, logRatio_nonneg, logRatio_pos, lt_normThreshold_zero, measure_gt_normThreshold_le_exp, measure_gt_normThreshold_le_rpow, measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self, normThreshold_add_one, normThreshold_eq, normThreshold_strictMono, normThreshold_zero, sq_normThreshold_add_one_le, tendsto_normThreshold_atTop, exists_integrable_exp_sq_of_map_rotation_eq_self, exists_integrable_exp_sq_of_map_rotation_eq_self', exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure, lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self, measure_le_mul_measure_gt_le_of_map_rotation_eq_self, exists_between_of_tendsto_atTop	23
Total	26

ContinuousLinearMap

Definitions

Name	Category	Theorems
rotation 📖	CompOp	3 math math: ProbabilityTheory.IsGaussian.map_rotation_eq_self, rotation_apply, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rotation_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField funLike rotation AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup 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.cos Real.sin Real.instNeg	—	—

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_integrable_exp_sq_of_map_rotation_eq_self 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod	Real.instLT Real.instZero MeasureTheory.Integrable Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_mul IsScalarTower.right MeasureTheory.Measure.restrict_univ cond_isProbabilityMeasure MeasureTheory.Measure.prod_smul_right MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure MeasureTheory.Measure.prod_smul_left smul_smul MeasureTheory.Measure.map_smul exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure MeasureTheory.integrable_smul_measure
exists_integrable_exp_sq_of_map_rotation_eq_self' 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod Real.instLT Real.instZero ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm AddMonoidWithOne.toOne	MeasureTheory.Integrable Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.measure_lt_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure lt_top_of_lt LE.le.trans_lt tsub_le_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero ENNReal.sub_lt_of_lt_add LT.lt.le two_mul mul_comm ENNReal.div_lt_iff NeZero.charZero_one inv_eq_one_div mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Fernique.logRatio_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Continuous.comp_aestronglyMeasurable Continuous.rexp continuous_id' MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.pow MeasureTheory.AEStronglyMeasurable.norm aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.abs_exp lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self le_rfl ENNReal.add_lt_top ENNReal.ofReal_lt_top Summable.tsum_ofReal_lt_top Real.summable_exp_nat_mul_of_ge mul_neg_of_neg_of_pos IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.instIsOrderedAddMonoid Real.instIsOrderedRing Real.instNontrivial Real.log_pos ENNReal.toReal_div ENNReal.toReal_lt_toReal LT.lt.ne Real.instZeroLEOneClass RCLike.charZero_rclike Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero
exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod	Real.instLT Real.instZero MeasureTheory.Integrable Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat exists_integrable_exp_sq_of_map_rotation_eq_self' le_antisymm MeasureTheory.prob_le_one MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Mathlib.Tactic.Push.not_and_eq not_le le_or_gt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass LE.le.trans le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Set.ext exists_nat_ge Real.instArchimedean Monotone.measure_iUnion instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike MeasureTheory.IsProbabilityMeasure.measure_univ one_mul ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero MeasureTheory.ae_iff_prob_eq_one measurable_to_prop Set.preimage_singleton_true measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal instSecondCountableTopologyReal Continuous.measurable Continuous.norm continuous_id' measurable_const MeasureTheory.integrable_of_le_of_le Continuous.comp_aestronglyMeasurable Continuous.rexp MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.pow MeasureTheory.AEStronglyMeasurable.norm aestronglyMeasurable_id MeasureTheory.ae_of_all Real.exp_pos Filter.mp_mem Filter.univ_mem' Real.exp_monotone pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono norm_nonneg MeasureTheory.integrable_const MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure
lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Preorder.toLT ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	MeasureTheory.lintegral ENNReal.ofReal Real.exp Real.instMul Fernique.logRatio Monoid.toNatPow Real.instMonoid Real.instInv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Real.log ENNReal.toReal ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Set.ext LT.lt.trans_le norm_nonneg MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.instCanonicallyOrderedAdd LE.le.eq_or_lt' inv_zero zero_pow Nat.instCharZero MulZeroClass.mul_zero MulZeroClass.zero_mul Real.exp_zero ENNReal.ofReal_one MeasureTheory.lintegral_const MeasureTheory.IsProbabilityMeasure.measure_univ mul_one ENNReal.toReal_div neg_mul le_add_right ENNReal.ofReal_le_ofReal Fernique.logRatio_nonneg LT.lt.le LE.le.trans MeasureTheory.prob_le_one MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Fernique.lintegral_exp_mul_sq_norm_le_mul one_mul mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid
measure_le_mul_measure_gt_le_of_map_rotation_eq_self 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instLT Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.instSub Real.sqrt	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod_prod MeasureTheory.Measure.map_apply ContinuousLinearMap.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right Prod.borelSpace MeasurableSet.inter measurableSet_le Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal Measurable.fun_comp Continuous.measurable Continuous.norm continuous_id' Measurable.fst measurable_id' measurable_const measurableSet_lt Measurable.snd Real.cos_neg Real.cos_pi_div_four Real.sin_neg Real.sin_pi_div_four neg_smul neg_neg norm_mul NormedDivisionRing.toNormMulClass norm_inv Real.norm_ofNat abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono le_of_lt Real.sqrt_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.sq_sqrt pow_two mul_inv mul_assoc inv_mul_cancel₀ ne_of_gt mul_one sub_eq_add_neg smul_sub norm_smul NormedSpace.toNormSMulClass div_eq_inv_mul smul_add MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass sub_lt_sub_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_le_sub_left div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_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 Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one 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.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos 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.mul_pf_right Mathlib.Tactic.Ring.mul_one norm_add_sub_norm_sub_le_two_mul_min le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true lt_min_iff le_refl

ProbabilityTheory.Fernique

Definitions

Name	Category	Theorems
logRatio 📖	CompOp	7 math math: ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self, lintegral_closedBall_diff_exp_logRatio_mul_sq_le, logRatio_mul_normThreshold_add_one_le, logRatio_pos, logRatio_nonneg, lintegral_exp_mul_sq_norm_le_mul, logRatio_mono
normThreshold 📖	CompOp	12 math math: lt_normThreshold_zero, normThreshold_zero, normThreshold_eq, lintegral_closedBall_diff_exp_logRatio_mul_sq_le, measure_gt_normThreshold_le_exp, logRatio_mul_normThreshold_add_one_le, measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self, measure_gt_normThreshold_le_rpow, normThreshold_strictMono, sq_normThreshold_add_one_le, normThreshold_add_one, tendsto_normThreshold_atTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_closedBall_diff_exp_logRatio_mul_sq_le 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm AddMonoidWithOne.toOne	Preorder.toLE MeasureTheory.lintegral MeasureTheory.Measure.restrict Set.instSDiff Metric.closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid normThreshold ENNReal.ofReal Real.exp Real.instMul logRatio Monoid.toNatPow Real.instMonoid Real.instInv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real.log ENNReal.toReal ENNReal.instDivInvMonoid ENNReal.instSub	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.setLIntegral_mono measurable_const ENNReal.ofReal_le_ofReal Real.exp_monotone mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono norm_nonneg dist_zero_right mul_nonneg LT.lt.le logRatio_pos Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE even_two_mul MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass mul_assoc measure_gt_normThreshold_le_exp mul_le_mul_left covariant_swap_mul_of_covariant_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_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.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 logRatio_mul_normThreshold_add_one_le mul_comm ENNReal.ofReal_mul le_of_lt Real.exp_pos Real.exp_add Nat.cast_one Nat.cast_pow ENNReal.toReal_div Mathlib.Tactic.Ring.add_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.pow_prod_atom 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isRat_mul
lintegral_exp_mul_sq_norm_le_mul 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod Real.instLT Real.instZero ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Preorder.toLT ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	MeasureTheory.lintegral ENNReal.ofReal Real.exp Real.instMul logRatio Monoid.toNatPow Real.instMonoid Real.instInv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toAdd tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Real.log ENNReal.toReal ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat LE.le.trans MeasureTheory.prob_le_one MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.setLIntegral_mono measurable_const ENNReal.ofReal_le_ofReal Real.exp_monotone mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono norm_nonneg dist_zero_right mul_nonneg logRatio_nonneg LT.lt.le le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter mul_comm inv_pow Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt 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 one_mul Mathlib.Tactic.FieldSimp.zpow'_one Set.ext ENNReal.toReal_div neg_mul le_add_right ENNReal.instCanonicallyOrderedAdd le_of_eq MeasureTheory.setLIntegral_univ MeasureTheory.setLIntegral_congr MeasureTheory.Measure.instOuterMeasureClass Filter.eventuallyEq_comm MeasureTheory.ae_eq_univ MeasureTheory.ae_iff Filter.mp_mem MeasureTheory.ae_iff_prob_eq_one measurable_to_prop Set.preimage_singleton_true measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal Continuous.measurable Continuous.norm continuous_id' Filter.univ_mem' lt_of_le_of_ne lt_of_le_of_lt le_or_gt StrictMono.exists_between_of_tendsto_atTop normThreshold_strictMono tendsto_normThreshold_atTop MeasureTheory.lintegral_union_le add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid MeasureTheory.lintegral_iUnion_le instCountableNat mul_add Distrib.leftDistribClass add_le_add covariant_swap_add_of_covariant_add ENNReal.tsum_mul_left Summable.tsum_le_tsum OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional le_trans MeasureTheory.lintegral_mono_fn' le_refl mul_le_mul_of_nonneg_right Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_pos Real.instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial logRatio_mono Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul lintegral_closedBall_diff_exp_logRatio_mul_sq_le LT.lt.trans_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Real.log_le_log div_pos ENNReal.toReal_pos_iff lt_trans Ne.lt_top ne_top_of_lt ENNReal.instOrderedSub ENNReal.sub_ne_top ENNReal.one_ne_top div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono ENNReal.toReal_nonneg ENNReal.toReal_mono MeasureTheory.measure_ne_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure tsub_le_tsub Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo ENNReal.summable
logRatio_mono 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne Preorder.toLE	Real Real.instLE logRatio	—	Nat.instAtLeastTwoHAddOfNat div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Real.log_le_log div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono ENNReal.toReal_pos_iff lt_trans LE.le.trans_lt Ne.lt_top ne_top_of_lt ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub ENNReal.sub_ne_top ENNReal.one_ne_top div_le_div₀ ENNReal.toReal_nonneg ENNReal.toReal_mono tsub_le_tsub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid le_refl le_of_lt mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo pow_pos IsStrictOrderedRing.toZeroLEOneClass add_pos' Real.instIsOrderedAddMonoid Nat.cast_one Real.sqrt_pos_of_pos
logRatio_mul_normThreshold_add_one_le 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne	Real Real.instLE Real.instMul logRatio Monoid.toNatPow Real.instMonoid normThreshold Real.instInv Real.instNatCast Real.log DivInvMonoid.toDiv Real.instDivInvMonoid ENNReal.toReal ENNReal.instSub	—	Nat.instAtLeastTwoHAddOfNat inv_zero zero_pow Nat.instCharZero MulZeroClass.mul_zero IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.log_nonneg one_le_div ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub Ne.lt_top ENNReal.sub_ne_top ENNReal.one_ne_top ENNReal.toReal_le_toReal ne_top_of_lt tsub_le_iff_left two_mul LT.lt.le mul_comm ENNReal.div_lt_iff ENNReal.instCharZero NeZero.charZero_one inv_eq_one_div mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono sq_normThreshold_add_one_le logRatio_pos le_of_lt lt_of_le_of_ne' Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass inv_ne_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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval 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_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Nat.cast_one Real.sqrt_pos_of_pos Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero 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.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isNat_mul
logRatio_nonneg 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne	Real Real.instLE Real.instZero logRatio	—	Nat.instAtLeastTwoHAddOfNat LE.le.eq_or_lt' ENNReal.toReal_inv ENNReal.toReal_ofNat ENNReal.one_sub_inv_two div_self RCLike.charZero_rclike Real.log_one zero_div tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub div_zero Real.log_zero LT.lt.le logRatio_pos
logRatio_pos 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne	Real Real.instLT Real.instZero logRatio	—	Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.log_pos one_lt_div_iff ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub Ne.lt_top ENNReal.sub_ne_top ENNReal.one_ne_top ENNReal.toReal_lt_toReal ne_top_of_lt ENNReal.sub_lt_of_lt_add LT.lt.le two_mul mul_comm ENNReal.div_lt_iff ENNReal.instCharZero NeZero.charZero_one inv_eq_one_div mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo pow_pos IsStrictOrderedRing.toZeroLEOneClass add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Real.sqrt_pos_of_pos
lt_normThreshold_zero 📖	mathematical	Real Real.instLT Real.instZero	DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat normThreshold	—	Nat.instAtLeastTwoHAddOfNat div_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add Real.instZeroLEOneClass RCLike.charZero_rclike
measure_gt_normThreshold_le_exp 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm AddMonoidWithOne.toOne	Preorder.toLE Real.instLT normThreshold Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real.exp Real.instMul Real.log ENNReal.toReal ENNReal.instDivInvMonoid ENNReal.instSub Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat lt_of_lt_of_le LT.lt.le MeasureTheory.measure_lt_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure lt_top_of_lt LE.le.trans_lt tsub_le_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero ENNReal.toReal_div div_pos_iff_of_pos_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LE.le.trans_eq measure_gt_normThreshold_le_rpow Real.log_inv mul_comm Real.log_rpow inv_pos_of_pos Real.exp_log Real.rpow_pos_of_pos ENNReal.ofReal_rpow_of_nonneg le_of_lt pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo inv_div ENNReal.ofReal_toReal ENNReal.div_ne_top ENNReal.sub_ne_top ENNReal.one_ne_top LT.lt.ne' lt_trans Nat.cast_one ENNReal.rpow_natCast
measure_gt_normThreshold_le_rpow 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	Preorder.toLE Real.instLT normThreshold Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.instDivInvMonoid ENNReal.instSub AddMonoidWithOne.toOne Nat.instMonoid	—	Nat.instAtLeastTwoHAddOfNat lt_of_lt_of_le LT.lt.le MeasureTheory.measure_lt_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure pow_zero pow_one ENNReal.mul_div_cancel LT.lt.ne' LT.lt.ne le_of_eq MeasureTheory.prob_compl_eq_one_sub measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal Continuous.measurable Continuous.norm continuous_id' measurable_const measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure mul_assoc ENNReal.inv_mul_cancel one_mul mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.pow_le_pow_left mul_pow pow_mul pow_two pow_add
measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self 📖	mathematical	MeasureTheory.Measure.map Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.rotation Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.prod	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instLT normThreshold Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat add_sub_cancel_right mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Real.instIsOrderedRing RCLike.charZero_rclike ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self
normThreshold_add_one 📖	mathematical	—	normThreshold Real Real.instAdd Real.instMul Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—
normThreshold_eq 📖	mathematical	—	normThreshold Real Real.instMul Real.instAdd Real.instOne Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat normThreshold.eq_1 arithGeom_same_eq_mul_div RCLike.charZero_rclike div_eq_mul_inv Real.inv_sqrt_two_sub_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right 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.zero_mul Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
normThreshold_strictMono 📖	mathematical	Real Real.instLT Real.instZero	StrictMono Nat.instPreorder Real.instPreorder normThreshold	—	arithGeom_strictMono Real.instIsStrictOrderedRing Real.one_lt_sqrt_two lt_normThreshold_zero
normThreshold_zero 📖	mathematical	—	normThreshold	—	—
sq_normThreshold_add_one_le 📖	mathematical	—	Real Real.instLE Monoid.toNatPow Real.instMonoid normThreshold Real.instMul Real.instAdd Real.instOne Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat normThreshold_eq mul_pow mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono zero_add Real.sq_sqrt covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike sub_le_sub_right pow_le_pow_right₀ add_le_add_left Nat.instIsOrderedAddMonoid Nat.instCanonicallyOrderedAdd sub_le_self pow_mul mul_comm le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass add_pos' Nat.cast_one Real.sqrt_pos_of_pos Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul
tendsto_normThreshold_atTop 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto normThreshold Filter.atTop Nat.instPreorder Real.instPreorder	—	tendsto_arithGeom_atTop_of_one_lt Real.instIsStrictOrderedRing Real.instArchimedean Real.one_lt_sqrt_two lt_normThreshold_zero

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_between_of_tendsto_atTop 📖	mathematical	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atTop Preorder.toLT	Preorder.toLE	—	Filter.tendsto_atTop_atTop_iff_of_monotone instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat monotone Nat.find_min Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.find_spec

---

← Back to Index