MeasureSpaceDef

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

Statistics

Metric	Count
Definitions mk, instFunLike, ofMeasurable, real, toOuterMeasure, toMeasurableSpace, volume, tacticVolume_tac, toMeasurable, «termAEMeasurable[_]», «termMeasure[_]_», «term∀ᵐ_,_», «term∃ᵐ_,_»	13
Theorems ae_eq_mk, eval, measurable_mk, of_discrete, aemeasurable, comp_aemeasurable, comp_aemeasurable', ae_induction_on_inter, coe_toOuterMeasure, ext, ext_iff, ext_iff', instOuterMeasureClass, m_iUnion, mono_null, ofMeasurable_apply, outerMeasure_le_iff, real_def, toOuterMeasure_apply, toOuterMeasure_injective, trim_le, trimmed, ae_le_toMeasurable, exists_measurable_superset, exists_measurable_superset_forall_eq, exists_measurable_superset_iff_measure_eq_zero, exists_measurable_superset_of_null, exists_measurable_superset₂, exists_measure_pos_of_not_measure_iUnion_null, measurableSet_toMeasurable, measureReal_def, measure_biUnion_lt_top, measure_biUnion_ne_top, measure_eq_extend, measure_eq_iInf, measure_eq_iInf', measure_eq_inducedOuterMeasure, measure_eq_trim, measure_inter_lt_top_of_left_ne_top, measure_inter_lt_top_of_right_ne_top, measure_inter_ne_top_of_left_ne_top, measure_inter_ne_top_of_right_ne_top, measure_inter_null_of_null_left, measure_inter_null_of_null_right, measure_le_measure_union_left, measure_le_measure_union_right, measure_lt_top_of_subset, measure_mono_top, measure_ne_top_of_subset, measure_symmDiff_ne_top, measure_toMeasurable, measure_union_eq_top_iff, measure_union_lt_top, measure_union_lt_top_iff, measure_union_ne_top, nonempty_of_measure_ne_zero, subset_toMeasurable, toMeasurable_def, toOuterMeasure_eq_inducedOuterMeasure, aemeasurable_congr, aemeasurable_const, aemeasurable_id, aemeasurable_id', aemeasurable_pi_iff, aemeasurable_pi_lambda	65
Total	78

AEMeasurable

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_mk 📖	mathematical	AEMeasurable	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
eval 📖	—	AEMeasurable MeasurableSpace.pi	—	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.eval Filter.Eventually.mono
measurable_mk 📖	mathematical	AEMeasurable	Measurable	—	MeasureTheory.Measure.instOuterMeasureClass
of_discrete 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable Measurable.of_discrete

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable 📖	mathematical	Measurable	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_refl
comp_aemeasurable 📖	—	Measurable AEMeasurable	—	—	MeasureTheory.Measure.instOuterMeasureClass comp Filter.EventuallyEq.fun_comp
comp_aemeasurable' 📖	—	Measurable AEMeasurable	—	—	comp_aemeasurable

MeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_induction_on_inter 📖	—	generateFrom IsPiSystem Filter.Eventually Set Set.instEmptyCollection MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem' induction_on_inter

MeasureTheory

Definitions

Name	Category	Theorems
tacticVolume_tac 📖	CompOp	—
toMeasurable 📖	CompOp	27 math math: Measure.restrict_toMeasurable, Measure.measure_toMeasurable_add_inter_right, Measure.measure_toMeasurable_add_inter_left, NullMeasurableSet.compl_toMeasurable_compl_ae_eq, Measure.measure_toMeasurable_inter, measure_biUnion_toMeasurable, Measure.restrict_toMeasurable_of_cover, pdf.IsUniform.toMeasurable, IntegrableOn.restrict_toMeasurable, Measure.measure_toMeasurable_inter_of_sFinite, ae_le_toMeasurable, pdf.IsUniform.toMeasurable_iff, Measure.restrict_inter_toMeasurable, subset_toMeasurable, Measure.measure_toMeasurable_inter_of_cover, measure_toMeasurable, ProbabilityTheory.cond_toMeasurable_eq, toMeasurable_def, measurableSet_toMeasurable, Measure.measure_toMeasurable_inter_of_sum, measure_trim_toMeasurable_eq_zero, nullMeasurableSet_toMeasurable, measure_union_toMeasurable, measure_toMeasurable_union, NullMeasurableSet.toMeasurable_ae_eq, measure_iUnion_toMeasurable, Measure.restrict_toMeasurable_of_sFinite
«termAEMeasurable[_]» 📖	CompOp	—
«termMeasure[_]_» 📖	CompOp	—
«term∀ᵐ_,_» 📖	CompOp	—
«term∃ᵐ_,_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_le_toMeasurable 📖	mathematical	—	Filter.EventuallyLE Prop.le ae Measure Measure.instFunLike Measure.instOuterMeasureClass toMeasurable	—	HasSubset.Subset.eventuallyLE Measure.instOuterMeasureClass subset_toMeasurable
exists_measurable_superset 📖	mathematical	—	Set Set.instHasSubset MeasurableSet DFunLike.coe Measure ENNReal Measure.instFunLike	—	OuterMeasure.exists_measurable_superset_eq_trim
exists_measurable_superset_forall_eq 📖	mathematical	—	Set Set.instHasSubset MeasurableSet DFunLike.coe Measure ENNReal Measure.instFunLike	—	OuterMeasure.exists_measurable_superset_forall_eq_trim
exists_measurable_superset_iff_measure_eq_zero 📖	mathematical	—	Set Set.instHasSubset MeasurableSet DFunLike.coe Measure ENNReal Measure.instFunLike instZeroENNReal	—	measure_mono_null Measure.instOuterMeasureClass exists_measurable_superset_of_null
exists_measurable_superset_of_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instHasSubset MeasurableSet	—	exists_measurable_superset
exists_measurable_superset₂ 📖	mathematical	—	Set Set.instHasSubset MeasurableSet DFunLike.coe Measure ENNReal Measure.instFunLike	—	exists_measurable_superset_forall_eq Bool.countable
exists_measure_pos_of_not_measure_iUnion_null 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike	—	Mathlib.Tactic.Contrapose.contrapose₂ measure_iUnion_null Measure.instOuterMeasureClass nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd
measurableSet_toMeasurable 📖	mathematical	—	MeasurableSet toMeasurable	—	Measure.instOuterMeasureClass exists_measurable_superset toMeasurable_def
measureReal_def 📖	mathematical	—	Measure.real ENNReal.toReal DFunLike.coe Measure Set ENNReal Measure.instFunLike	—	—
measure_biUnion_lt_top 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Top.top instTopENNReal	Set.iUnion Set.instMembership	—	Set.ext Set.Finite.mem_toFinset LE.le.trans_lt measure_biUnion_finset_le Measure.instOuterMeasureClass
measure_biUnion_ne_top 📖	—	—	—	—	LT.lt.ne measure_biUnion_lt_top Ne.lt_top
measure_eq_extend 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike extend	—	extend_eq
measure_eq_iInf 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.instHasSubset MeasurableSet	—	measure_eq_trim OuterMeasure.trim_eq_iInf Measure.coe_toOuterMeasure
measure_eq_iInf' 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike iInf Set.instHasSubset MeasurableSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	iInf_subtype iInf_congr_Prop iInf_and
measure_eq_inducedOuterMeasure 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike OuterMeasure OuterMeasure.instFunLikeSetENNReal inducedOuterMeasure MeasurableSet MeasurableSet.empty OuterMeasure.empty Measure.toOuterMeasure	—	measure_eq_trim
measure_eq_trim 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike OuterMeasure OuterMeasure.instFunLikeSetENNReal OuterMeasure.trim Measure.toOuterMeasure	—	Measure.trimmed Measure.coe_toOuterMeasure
measure_inter_lt_top_of_left_ne_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.instInter Top.top instTopENNReal	—	Ne.lt_top measure_inter_ne_top_of_left_ne_top
measure_inter_lt_top_of_right_ne_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.instInter Top.top instTopENNReal	—	Ne.lt_top measure_inter_ne_top_of_right_ne_top
measure_inter_ne_top_of_left_ne_top 📖	—	—	—	—	measure_ne_top_of_subset Set.inter_subset_left
measure_inter_ne_top_of_right_ne_top 📖	—	—	—	—	measure_ne_top_of_subset Set.inter_subset_right
measure_inter_null_of_null_left 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instInter	—	measure_mono_null Measure.instOuterMeasureClass Set.inter_subset_left
measure_inter_null_of_null_right 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instInter	—	measure_mono_null Measure.instOuterMeasureClass Set.inter_subset_right
measure_le_measure_union_left 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.instUnion	—	OuterMeasure.mono Set.subset_union_left
measure_le_measure_union_right 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.instUnion	—	OuterMeasure.mono Set.subset_union_right
measure_lt_top_of_subset 📖	mathematical	Set Set.instHasSubset	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike Top.top instTopENNReal	—	lt_of_le_of_lt OuterMeasure.mono Ne.lt_top
measure_mono_top 📖	—	Set Set.instHasSubset DFunLike.coe Measure ENNReal Measure.instFunLike Top.top instTopENNReal	—	—	top_unique measure_mono Measure.instOuterMeasureClass
measure_ne_top_of_subset 📖	—	Set Set.instHasSubset	—	—	LT.lt.ne measure_lt_top_of_subset
measure_symmDiff_ne_top 📖	—	—	—	—	ne_top_of_le_ne_top measure_union_ne_top measure_mono Measure.instOuterMeasureClass Set.symmDiff_subset_union
measure_toMeasurable 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike toMeasurable	—	Measure.instOuterMeasureClass exists_measurable_superset toMeasurable_def measure_congr Set.inter_univ MeasurableSet.univ
measure_union_eq_top_iff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion Top.top instTopENNReal	—	not_iff_not
measure_union_lt_top 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Top.top instTopENNReal	Set.instUnion	—	LE.le.trans_lt measure_union_le Measure.instOuterMeasureClass ENNReal.add_lt_top
measure_union_lt_top_iff 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.instUnion Top.top instTopENNReal	—	LE.le.trans_lt measure_mono Measure.instOuterMeasureClass Set.subset_union_left Set.subset_union_right measure_union_lt_top
measure_union_ne_top 📖	—	—	—	—	LT.lt.ne measure_union_lt_top Ne.lt_top
nonempty_of_measure_ne_zero 📖	mathematical	—	Set.Nonempty	—	Set.nonempty_iff_ne_empty measure_empty Measure.instOuterMeasureClass
subset_toMeasurable 📖	mathematical	—	Set Set.instHasSubset toMeasurable	—	Measure.instOuterMeasureClass exists_measurable_superset toMeasurable_def
toMeasurable_def 📖	mathematical	—	toMeasurable Set Set.instHasSubset MeasurableSet Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal DFunLike.coe exists_measurable_superset	—	Measure.instOuterMeasureClass exists_measurable_superset
toOuterMeasure_eq_inducedOuterMeasure 📖	mathematical	—	Measure.toOuterMeasure inducedOuterMeasure MeasurableSet DFunLike.coe Measure Set ENNReal Measure.instFunLike MeasurableSet.empty OuterMeasure.empty	—	Measure.trimmed

MeasureTheory.Measure

Definitions

Name	Category	Theorems
instFunLike 📖	CompOp	2277 math math: MeasureTheory.exists_pos_preimage_ball, ProbabilityTheory.Kernel.restrict_apply', prod_apply_symm, AddCircle.measure_univ, MeasureTheory.predictablePart_add_ae_eq, MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal, MeasureDense.approx, MeasureTheory.Integrable.measure_norm_gt_lt_top_enorm, MeasureTheory.AEEqFun.coeFn_smul, univ_pi_Ioc_ae_eq_Icc, MeasureTheory.LpToLpRestrictCLM_coeFn, bind_apply, VitaliFamily.FineSubfamilyOn.measure_diff_biUnion, ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, MeasureTheory.vaddInvariantMeasure_iff, ProbabilityTheory.Kernel.prod_apply', MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, ProbabilityTheory.Kernel.tendsto_m_density, ProbabilityTheory.absolutelyContinuous_posterior_iff, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm', MeasureTheory.llr_self, StieltjesFunction.measure_univ_of_tendsto_atBot_atBot, restrict_singleton, MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ, ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable, ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul, ProbabilityTheory.condCDF_ae_eq, sum_apply_eq_zero', ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter, MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior, MeasureTheory.ae_withDensity_iff_ae_restrict, ProbabilityTheory.lintegral_condCDF, rnDeriv_zero, addHaar_eq_zero_of_disjoint_translates, MonotoneOn.ae_differentiableWithinAt_of_mem, MeasureTheory.SimpleFunc.sum_measure_preimage_singleton, MeasureTheory.iInf_mul_le_lintegral, addHaar_image_continuousLinearMap, MeasureTheory.withDensity_apply_le, MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq, ProbabilityTheory.condDistrib_apply_of_ne_zero, MeasureTheory.forall_measure_preimage_add_iff, PMF.toMeasure_pure_apply, ProbabilityTheory.condDistrib_ae_eq_condExp, MeasureTheory.coe_measureUnivNNReal, aeconst_of_dense_aestabilizer_smul, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, le_comap_apply, addHaar_sphere, MeasureTheory.hausdorffMeasure_segment, InnerProductSpace.volume_closedBall_of_dim_even, MeasureTheory.lintegral_const, ProbabilityTheory.IsCondKernelCDF.toKernel_Iic, ae_ennreal_smul_measure_eq, MeasureTheory.measure_sdiff_inv_smul, MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, MeasureTheory.Integrable.measure_enorm_ge_lt_top, haar_singleton, unitInterval.volume_Ioo, unitInterval.volume_Iic, MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator, MeasureTheory.AEEqFun.comp₂Measurable_toGerm, MeasureTheory.Integrable.toL1_eq_toL1_iff, ProbabilityTheory.lintegral_toKernel_univ, rnDeriv_smul_right', MeasureTheory.eLpNorm'_const', MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, volume_iUnion_setOf_liouvilleWith, MeasureTheory.Submartingale.upcrossings_ae_lt_top, ProbabilityTheory.condIndep_iff, IsAddFoelner.eventually_meas_ne_top, StieltjesFunction.measure_botSet, MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable, MeasureTheory.Integrable.withDensityᵥ_eq_iff, ContinuousMap.coeFn_toAEEqFun, MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst, hausdorffMeasure_zero_singleton, AntilipschitzWith.hausdorffMeasure_preimage_le, ProbabilityTheory.Kernel.borelMarkovFromReal_apply', MeasureTheory.lintegral_eq_zero_iff, ProbabilityTheory.Kernel.iIndep.meas_biInter, MeasureTheory.vadd_ae, ProbabilityTheory.IsRatCondKernelCDF.iInf_rat_gt_eq, ProbabilityTheory.Kernel.density_fst_univ, AbsolutelyContinuousOnInterval.ae_differentiableAt, ext_iff, ContinuousLinearMap.comp_condExp_comm, rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular, ProbabilityTheory.setLIntegral_preCDF_fst, VitaliFamily.withDensity_le_mul, MeasureTheory.pdf.uniformPDF_ite, MeasureTheory.MeasuredSets.sub_le_edist, measure_mono_both, lintegral_rnDeriv, LipschitzOnWith.ae_differentiableWithinAt_of_mem, MeasureTheory.measure_compl_sigmaFiniteSet, MeasureTheory.ae_le_const_iff_forall_gt_measure_zero, MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, MeasureTheory.setLIntegral_le_iSup_mul, measure_le_lintegral_thickenedIndicatorAux, rnDeriv_mul_rnDeriv', VitaliFamily.le_mul_withDensity, outerMeasure_le_iff, PMF.toMeasure_bind_apply, MeasurableEmbedding.rnDeriv_map, MeasureTheory.AEEqFun.toGerm_injective, ProbabilityTheory.Kernel.condExp_traj', MeasureTheory.Lp.coeFn_add, pi_Ioc_ae_eq_pi_Icc, AbsolutelyContinuous.kernel_of_compProd, ProbabilityTheory.iIndepFun_iff, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone, PMF.toMeasure_ofFinset_apply, rnDeriv_add_of_mutuallySingular, MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet, inv_rnDeriv', MeasureTheory.Lp.eq_zero_iff_ae_eq_zero, StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop, LocallyIntegrable.ae_hasDerivAt_integral, ProbabilityTheory.iIndep.meas_biInter, mutuallySingular_tfae, ae_eq_const_or_exists_average_ne_compl, MeasureTheory.measure_eq_top_iff_of_symmDiff, measure_isMulLeftInvariant_eq_smul_of_ne_top, count_injective_image', MeasureTheory.Lp.ext_iff, MeasureTheory.ae_restrict_mem, MeasureTheory.measure_inv_null, MeasureTheory.condLExp_add_right, MeasureTheory.measure_biUnion, MeasureTheory.setLIntegral_pos_iff, comp_apply_univ, ProbabilityTheory.Kernel.swapRight_apply', MeasureTheory.UniformIntegrable.uniformIntegrable_of_ae_tendsto, LipschitzWith.ae_lineDeriv_sum_eq, ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, measure_subtype_coe_le_comap, MeasureTheory.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds, Filter.HasBasis.notMem_measureSupport, MeasureTheory.smul_le_stoppedValue_hittingBtwn, MeasureTheory.Lp.coeFn_const, measure_toMeasurable_add_inter_right, ProbabilityTheory.rnDeriv_gaussianReal, MeasureTheory.measure_le_setLAverage_pos, MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real, MeasureTheory.measure_preimage_mul, toSphere_apply_aux, pi'_pi, MeasureTheory.measure_diff_le_iff_le_add, MeasureTheory.SimpleFunc.measure_support_lt_top_of_memLp, MeasureTheory.Integrable.measure_norm_ge_lt_top, ProbabilityTheory.Kernel.trajContent_cylinder, IsOpen.measure_eq_iSup_isClosed, MeasureTheory.tendsto_measure_iUnion_atBot, ae_mem_finset_iff, MeasureTheory.mem_ae_map_iff, MeasureTheory.AEEqFun.mk_le_mk, ProbabilityTheory.cond_apply, MeasureTheory.meas_le_lintegral₀, haarMeasure_closure_self, ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, ProbabilityTheory.sum_prob_mem_Ioc_le, MeasureTheory.AEEqFun.coeFn_inf, measurable_measure, MeasureTheory.measure_preimage_fst_singleton_eq_tsum, isTopologicalBasis_isOpen_lt_top, ProbabilityTheory.boolKernel_comp_measure, haarMeasure_apply, MeasureTheory.exp_llr_of_ac', MeasureTheory.measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed, MeasureTheory.IsFundamentalDomain.measure_set_eq, MeasurableEquiv.map_apply, ProbabilityTheory.Kernel.IndepSets.indep_aux, MeasureTheory.lintegral_indicator_one_le, MeasureTheory.AEEqFun.coeFn_mul, measure_univ_pos, LipschitzWith.ae_exists_fderiv_of_countable, MeasureTheory.AEEqFun.neg_toGerm, Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, MeasureTheory.eLpNorm_const_lt_top_iff_enorm, ContinuousLinearMap.comp_condExp_add_const_comm, ae_ne, MeasureTheory.ae_restrict_biUnion_iff, MeasureTheory.toReal_rnDeriv_tilted_left, MeasureTheory.tilted_neg_same', MeasureTheory.AEEqFun.coeFn_comp₂, le_ae_join, ProbabilityTheory.sum_meas_smul_cond_fiber, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_memLp_exp_mul, ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range, domSMul_apply, ProbabilityTheory.iIndepFun.measure_inter_preimage_eq_mul, MeasureTheory.condLExp_bot', MeasureTheory.AddContent.measure_eq, IsFoelner.eventually_meas_ne_zero, StieltjesFunction.measure_Ici_of_tendsto_atTop_atTop, coe_nnreal_smul_apply, Real.volume_closedEBall, comapₗ_eq_comap, unitInterval.volume_Ico, MeasureTheory.measure_eq_top_of_setLIntegral_ne_top, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.measure_compl, MulAction.mem_aestabilizer, IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul, MeasureTheory.measure_compl_sigmaFiniteSetWRT, haarMeasure_unique, Isometry.hausdorffMeasure_image, VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas, ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq, MeasureTheory.ae_uIoc_iff, count_apply, MeasureTheory.condLExp_smul, MeasureTheory.MemLp.toLp_eq_toLp_iff, ae_eq_zero_of_integral_contMDiff_smul_eq_zero, StieltjesFunction.measure_Ioo, MeasureTheory.hasFiniteIntegral_prod_iff', measure_toMeasurable_add_inter_left, measure_preimage_neg, MeasureTheory.measure_support_eapprox_lt_top, ProbabilityTheory.bayesRisk_of_subsingleton', rnDeriv_smul_right, rnDeriv_smul_left_of_ne_top', ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, ProbabilityTheory.uniformOn_inter, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, sum_smul_dirac, MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT', ae_mem_finset_iff_map_eq_sum_dirac, PMF.toMeasure_apply_singleton, LocallyBoundedVariationOn.ae_differentiableWithinAt, Directed.measure_iUnion, unitInterval.volume_apply, ProbabilityTheory.uniformOn_of_univ, MeasureTheory.exists_measurable_superset₂, le_sum_apply, ProbabilityTheory.Kernel.compProd_null, Real.volume_closedBall, ProbabilityTheory.tilted_mul_apply_cgf, Besicovitch.exists_closedBall_covering_tsum_measure_le, IsCompact.measure_closure, MeasureTheory.setLIntegral_eq_const, IsOpen.measure_zero_iff_eq_empty, MeasureTheory.prob_compl_eq_one_iff₀, measurable_coe, restrict_apply_self, MeasureTheory.ae_restrict_biUnion_eq, MeasureTheory.pdf.eq_of_map_eq_withDensity, MeasureTheory.eventuallyConst_inv_set_ae, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image, MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero, MeasureTheory.mul_meas_ge_le_pow_eLpNorm', abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, map_fst_prod, MeasureTheory.exists_null_pairwise_disjoint_diff, addHaar_ball_of_pos, Real.volume_val, MeasureTheory.volume_pi_pi, rnDeriv_restrict, MeasureTheory.lintegral_singleton, haarMeasure_self, PMF.toMeasure_ofFintype_apply, MeasureTheory.Conservative.frequently_measure_inter_ne_zero, MeasureTheory.lintegral_countable, mkMetric_apply, ProbabilityTheory.Kernel.IsCondKernel.isProbabilityMeasure_ae, addHaar_eq_zero_of_disjoint_translates_aux, count_singleton', ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop, Real.volume_pi_ball, const_comp, iInf_IicSnd_gt, MeasureTheory.biSup_measure_Iic, MeasureTheory.measurable_measure_add_right, sum_apply_of_countable, ProbabilityTheory.Kernel.rnDeriv_eq_one_iff_eq, NumberField.mixedEmbedding.convexBodyLT_volume, MeasureTheory.measure_integral_le_pos, MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant, MeasureTheory.withDensity_apply_eq_zero, addHaar_preimage_smul, MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite, PMF.toMeasure_apply, MeasureTheory.laverage_eq', MeasureTheory.condLExp_add_left, MeasureTheory.withDensity_eq_zero_iff, PMF.toMeasure_ofMultiset_apply, Complex.volume_sum_rpow_le, MeasureTheory.ae_measure_preimage_mul_right_lt_top, MeasureTheory.enorm_ae_le_eLpNormEssSup, addHaar_sphere_of_ne_zero, ProbabilityTheory.Kernel.ae_compProd_iff, MeasureTheory.MeasurePreserving.measure_preimage_emb, MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq, MeasureTheory.meas_eLpNormEssSup_lt, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, MeasurableSet.exists_isCompact_isClosed_diff_lt, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero', ProbabilityTheory.cond_apply_self, MeasureTheory.MemLp.meas_ge_lt_top, MeasureTheory.Ioo_ae_eq_Icc, LocallyBoundedVariationOn.ae_differentiableAt, MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero, MeasureTheory.isFiniteMeasure_iff, hausdorffMeasure_le_liminf_sum, MeasureTheory.measure_inter_add_diff₀, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, ProbabilityTheory.Kernel.deterministic_prod_apply', MeasureTheory.measure_smul_eq_zero_iff, MeasureTheory.FiniteMeasure.restrict_apply_measure, MeasureTheory.tendsto_measure_biInter_gt, comap_preimage, pi_hyperplane, PreErgodic.ae_eq_const_of_ae_eq_comp, MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq, univ_pi_Ioo_ae_eq_Icc, MeasureTheory.measure_lt_one_eq_integral_div_gamma, MeasureTheory.div_ae_eq_one, ProbabilityTheory.cond_pos_of_inter_ne_zero, MeasureTheory.meas_le_ae_eq_meas_lt, forall_measure_inter_spanningSets_eq_zero, MeasureTheory.Supermartingale.le_zero_of_predictable, toENNRealVectorMeasure_apply, rnDeriv_eq_one_iff_eq, MeasureTheory.measure_neg_vadd_inter, ProbabilityTheory.Kernel.isIrreducible_iff, MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, addHaarMeasure_closure_self, MeasureTheory.SimpleFunc.restrict_lintegral, StieltjesFunction.measure_singleton, MeasureTheory.tendsto_measure_iUnion_atTop, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite, support_mem_ae_of_isLindelof, ae_sum_iff, MeasureTheory.SignedMeasure.eq_rnDeriv, Continuous.ae_eq_iff_eq, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, ProbabilityTheory.condExp_ae_eq_integral_condDistrib, MeasureTheory.ae_isMeasurablyGenerated, nullMeasurableSet_prod, ProbabilityTheory.Kernel.map_apply', setLIntegral_rnDeriv, ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self, MeasureTheory.piContent_cylinder, map_apply, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, ApproximatesLinearOn.norm_fderiv_sub_le, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, addHaar_ball_mul, MeasurableEquiv.comap_apply, MeasureTheory.Integrable.measure_ge_lt_top, LipschitzOnWith.ae_differentiableWithinAt_of_mem_real, ProbabilityTheory.posterior_boolKernel_apply_true, MeasureTheory.isProbabilityMeasureSMul, MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT, IsCompact.exists_open_superset_measure_lt_top', measure_toMeasurable_inter, ProbabilityTheory.Kernel.parallelComp_apply_prod, MeasureTheory.measure_lt_top, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq, MeasureTheory.indicatorConstLp_coeFn_mem, MeasureTheory.eventuallyConst_smul_set_ae, MeasureTheory.condExpL1_of_aestronglyMeasurable', MeasureTheory.map_mul_left_ae, IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div, MeasureTheory.IsFundamentalDomain.covolume_eq_volume, ProbabilityTheory.avgRisk_le_mul', ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero, blimsup_thickening_mul_ae_eq_aux, MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint, MeasureTheory.AEEqFun.coeFn_neg, ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp, MeasureTheory.lintegral_indicator_const_comp, ProbabilityTheory.Kernel.iIndepSet.meas_biInter, Monotone.ae_differentiableAt, comp_eq_sum_of_countable, ProbabilityTheory.iCondIndep_iff, MeasureTheory.measure_biUnion_toMeasurable, MeasureTheory.condExpL2_indicator_ae_eq_smul, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, MeasureTheory.Filtration.condExp_condExp, VitaliFamily.FineSubfamilyOn.measure_le_tsum, MeasureTheory.ae_eq_condLExp, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, prod_prod_le, MeasureTheory.Integrable.measure_lt_lt_top, curveIntegralFun_trans_aeeq_right, MeasureTheory.addEquivAddHaarChar_smul_preimage, ProbabilityTheory.iIndepSets.meas_iInter, MeasureTheory.AEStronglyMeasurable.prodMk_right, MeasureTheory.AEEqFun.coeFn_sub, pi_pi_aux, StieltjesFunction.measure_univ, MeasureTheory.integrableOn_const_iff, EuclideanSpace.volume_closedBall_fin_three, MeasureTheory.measure_inter_lt_top_of_right_ne_top, ProbabilityTheory.measurable_condDistrib, MeasureTheory.AEEqFun.coeFn_le, discard_comp, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, MeasureTheory.map_add_left_ae, MeasureTheory.measure_preimage_vadd_of_nullMeasurableSet, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, MeasureTheory.measurable_measure_mul_right, MeasureTheory.Integrable.ae_of_compProd, MeasureTheory.rnDeriv_conv, Real.volume_preimage_mul_left, MeasureTheory.IsAddFundamentalDomain.measure_eq, MeasureTheory.memLp_const_iff, restrict_eq_zero, ProbabilityTheory.Kernel.tendsto_density_atTop_ae_of_antitone, Real.volume_pi_Ico, MeasureTheory.ae_add_measure_iff, mkMetric_le_liminf_tsum, IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd, MeasureTheory.measure_mul_right_null, hausdorffMeasure_mono, Metric.measure_closedBall_pos_iff, MeasureTheory.ae_zero, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul, MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc, volume_setOf_liouville, rnDeriv_smul_left_of_ne_top, MeasureTheory.measure_sigmaFiniteSetGE_le, mem_cofinite, MeasureTheory.integral_eq_zero_iff_of_nonneg, MeasureTheory.condExp_smul_of_aestronglyMeasurable_right, NNReal.count_const_le_le_of_tsum_le, toOuterMeasure_apply, ProbabilityTheory.setBernoulli_singleton, MeasureTheory.inv_ae, ProbabilityTheory.Kernel.piecewise_apply', MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset, MeasureTheory.union_ae_eq_left_iff_ae_subset, MulAction.aeconst_of_aestabilizer_eq_top, MeasurableSet.exists_isCompact_lt_add, restrict_apply_superset, MeasureTheory.tendsto_measure_of_tendsto_indicator, MeasureTheory.SimpleFunc.const_lintegral_restrict, ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul, ProbabilityTheory.Kernel.compProd_deterministic_apply, MeasureTheory.AEEqFun.coeFn_comp, MeasureTheory.tendstoInMeasure_iff_norm, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, MeasureTheory.Content.measure_eq_content_of_regular, addHaar_unitClosedBall_eq_addHaar_unitBall, count_apply_eq_top, VitaliFamily.measure_limRatioMeas_zero, ProbabilityTheory.Kernel.rnDeriv_singularPart, ProbabilityTheory.Indep_iff, MeasureTheory.AEEqFun.toGerm_eq, ProbabilityTheory.condIndepSets_singleton_iff, BoundedVariationOn.ae_differentiableAt_of_mem_uIcc, MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc, Real.volume_Icc_pi, ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self, MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd, infinitePi_pi, BoundedContinuousFunction.lintegral_nnnorm_le, IsFoelner.tendsto_meas_smul_symmDiff, MeasureTheory.AEEqFun.coeFn_const, MeasureTheory.measure_mul_measure_eq, ae_differentiableAt_norm, ProbabilityTheory.indepSets_singleton_iff, MeasureTheory.addMeasure_map_restrict_apply, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, ProbabilityTheory.Kernel.compProd_eq_tsum_compProd, VitaliFamily.ae_tendsto_lintegral_div, VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', AEMeasurable.ae_of_bind, smul_measure_isAddInvariant_le_of_isCompact_closure, MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg, IsometryEquiv.hausdorffMeasure_image, MeasureTheory.measure_inv_smul_sdiff, ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.llr_tilted_right, MeasureTheory.measure_neg_null, MeasureTheory.pdf.uniformPDF_eq_pdf, MeasureTheory.condExp_mul_of_aestronglyMeasurable_right, comapₗ_apply, MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet, StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot, MeasureTheory.AEStronglyMeasurable.comp, MeasureTheory.sub_ae_eq_zero, ProbabilityTheory.uniformOn_empty, MeasureTheory.eLpNorm_eq_zero_iff, ProbabilityTheory.strong_law_ae, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, PreErgodic.measure_self_or_compl_eq_zero, IsClosed.measure_eq_one_iff_eq_univ, MeasureTheory.condExpIndSMul_empty, MeasureTheory.measure_vadd, MeasureTheory.prob_le_one, MeasureTheory.measure_union_lt_top_iff, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, coeAddHom_apply, MeasureTheory.Martingale.eq_zero_of_predictable, measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq, aestronglyMeasurable_iff_aemeasurable_separable, Real.volume_singleton, restrict_apply, MeasureTheory.measure_lintegral_le_pos, ae_sum_eq, mutuallySingular_of_mutuallySingular_compProd, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_pos_eq_zero_of_hasSubGaussianMGF_zero, BoxIntegral.Box.measure_coe_lt_top, ProbabilityTheory.iIndepFun.meas_biInter, MeasureTheory.map_sub_right_ae, StieltjesFunction.measure_univ_of_tendsto_atTop_atTop, AddCircle.add_projection_respects_measure, LipschitzWith.ae_lineDifferentiableAt, ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1, MeasureDense.fin_meas_approx, MeasureTheory.lintegral_le_iSup_mul, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite, MeasureTheory.Integrable.measure_gt_lt_top, rnDeriv_mul_rnDeriv, ProbabilityTheory.stronglyMeasurable_condExpKernel, ProbabilityTheory.setBernoulli_apply', MeasureTheory.Integrable.tendsto_ae_condExp, ProbabilityTheory.iIndepSets_iff, mutuallySingular_compProd_right_iff, MeasureTheory.exists_pos_measure_of_cover, blimsup_cthickening_ae_le_of_eventually_mul_le_aux, Real.volume_pi_Ioc, ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_top, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range, aeconst_of_dense_setOf_preimage_smul_eq, MeasureTheory.ae_toFinite, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero, BoxIntegral.Box.measure_Icc_lt_top, MeasureTheory.AEEqFun.compMeasurable_toGerm, map_restrict_ae_le_map_indicator_ae, Real.volume_emetric_closedBall, MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, MeasureTheory.mem_ae_dirac_iff, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, rnDeriv_lt_top, ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.prob_compl_eq_one_sub₀, Besicovitch.ae_tendsto_rnDeriv, Ergodic.iff_mem_extremePoints_measure_univ_eq, addHaarMeasure_eq_iff, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd, MeasureTheory.pdf.IsUniform.measure_preimage, count_eq_zero_iff, ProbabilityTheory.condVar_smul, MeasureTheory.map_add_right_ae, MeasureTheory.prob_compl_eq_one_iff, MeasureTheory.ae_withDensity_iff_ae_restrict', ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, MeasureTheory.measure_univ_of_isMulLeftInvariant, MeasureTheory.ae_restrict_iUnion_eq, Real.volume_ball, addHaar_preimage_continuousLinearMap, ae_prod_iff_ae_ae, MeasureTheory.condExp_finset_sum, Real.volume_Icc_pi_toReal, eq_rnDeriv, MeasureTheory.AEEqFun.liftRel_mk_mk, map_div_left_ae, IsFoelner.eventually_meas_ne_top, prod_apply_le, ProbabilityTheory.Kernel.le_compProd_apply, MeasureTheory.ae_mono, MeasureTheory.ae_restrict_mem₀, ProbabilityTheory.ofReal_condCDF_ae_eq, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, dirac_apply', countable_meas_pos_of_disjoint_iUnion₀, coe_toOuterMeasure, MeasureTheory.volume_sum_rpow_lt, unitInterval.volume_uIcc, ProbabilityTheory.Kernel.aestronglyMeasurable_traj, ZSpan.volume_fundamentalDomain, MeasureTheory.condExp_neg, MeasureTheory.condExp_mul_of_stronglyMeasurable_right, unitInterval.volume_Ici, MeasureTheory.measure_singleton_lt_top, MeasureTheory.SimpleFunc.restrict_const_lintegral, ProbabilityTheory.Kernel.iIndepSets.meas_biInter, MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant, ZSpan.measure_fundamentalDomain, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image, ProbabilityTheory.condExpKernel_ae_eq_condExp', MeasureTheory.hahn_decomposition, MeasureTheory.ae_withDensity_iff, MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eq_iff, MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq_iff, MeasureTheory.Integrable.condKernel_ae, innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group, ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup, addHaar_ball_center, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure, MeasurableSet.exists_isCompact_diff_lt, MeasureTheory.lintegral_eq_zero_iff', MeasureTheory.ae_restrict_eq_bot, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map, MeasureTheory.tendstoInMeasure_iff_dist, measure_toMeasurable_inter_of_sFinite, toSphere_apply_univ, MeasurableSet.measure_eq_iSup_isCompact, MeasureTheory.Lp.coeFn_compMeasurePreserving, MeasureTheory.measure_symmDiff_le, unitInterval.volume_uIoo, MeasureTheory.laverage_eq, MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero, MeasurableEmbedding.rnDeriv_map_aux, liftLinear_apply₀, hausdorffMeasure_smul₀, MeasureTheory.ae_ae_add_linearMap_mem_iff, ProbabilityTheory.HasLaw.ae_iff, Monotone.ae_hasDerivAt, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, RealRMK.rieszMeasure_le_of_eq_one, MeasureTheory.condExp_condExp_of_le, EuclideanSpace.volume_closedBall_fin_two, MeasureTheory.enorm_indicatorConstLp_le, MeasureTheory.AEEqFun.coeFn_abs, ProbabilityTheory.tsum_prob_mem_Ioi_lt_top, exists_spanning_measurableSet_le, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, essSup_eq_sInf, Real.volume_pi_Ioc_toReal, MeasureTheory.FiniteMeasure.coeFn_def, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1, tendsto_measure_cthickening, ProbabilityTheory.Kernel.ae_kernel_lt_top, MeasureTheory.vadd_set_ae_le, absolutelyContinuous_comp_of_countable, VitaliFamily.ae_tendsto_limRatio, MeasureTheory.measure_sdiff_neg_vadd, ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel, MeasureTheory.measure_compl_le_add_iff, IsOpen.measure_pos, condKernel_apply_of_ne_zero, Set.exists_isOpen_lt_add, MeasureTheory.withDensity_apply_eq_zero', ProbabilityTheory.Kernel.rnDeriv_ne_top, MeasureTheory.condExp_ofNat, tendsto_measure_Icc, MeasureTheory.SimpleFunc.lintegral_restrict, MeasureTheory.measure_union_add_inter, BoxIntegral.Box.coe_ae_eq_Icc, prod_apply, MeasureTheory.measure_laverage_le_pos, MeasureTheory.Lp.coeFn_smul, Real.volume_Iio, InnerRegularWRT.of_sigmaFinite, UnitAddCircle.measure_univ, InformationTheory.klDiv_zero_left, MeasureTheory.measure_biUnion_eq_iSup, MeasureTheory.measure_neg_vadd_symmDiff, MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving, addHaarMeasure_unique, ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk, AEMeasurable.ae_inf_principal_eq_mk, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, compProd_apply_univ, MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.eventually_mul_left_iff, Set.Countable.ae_notMem, pi_ball, ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul, ProbabilityTheory.IsRatCondKernelCDFAux.mono, le_iff', MeasurableSet.exists_isClosed_lt_add, Besicovitch.exist_finset_disjoint_balls_large_measure, mem_support_iff, MeasureTheory.measure_le_measure_union_left, ae_prod_mem_iff_ae_ae_mem, map_sub_left_ae, RealRMK.measure_le_of_isCompact_of_integral, blimsup_cthickening_ae_le_of_eventually_mul_le, BoxIntegral.Box.Ioo_ae_eq_Icc, PMF.toMeasure_apply_eq_toOuterMeasure_apply, compProd_apply, MeasureTheory.IsProjectiveLimit.measure_univ_eq, Filter.Eventually.volume_pos_of_nhds_real, lintegral_rnDeriv_le, MeasureTheory.AEDisjoint.diff_ae_eq_right, MeasureTheory.Lp.coeFn_le, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf', ProbabilityTheory.condIndepSet_iff, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, MeasureTheory.Lp.simpleFunc.add_toSimpleFunc, MeasureTheory.ae_le_toMeasurable, ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map, UnitAddTorus.coeFn_mFourierLp, PMF.toOuterMeasure_apply_le_toMeasure_apply, MeasureTheory.Ioi_ae_eq_Ici, sum_apply, ext_prod₃_iff', MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, ProbabilityTheory.IsCondKernelCDF.setLIntegral, MeasureTheory.measure_le_laverage_pos, lt_iff', MeasureTheory.AEEqFun.ext_iff, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg, Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux, rnDeriv_smul_left', MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero', MeasureTheory.condExp_mul_of_aestronglyMeasurable_left, MeasureTheory.projectiveFamilyContent_cylinder, MeasureTheory.IsAddFundamentalDomain.measure_set_eq, Antitone.measure_iUnion, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf', ProbabilityTheory.Kernel.finset_sum_apply', MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg, ProbabilityTheory.Kernel.pow_add_apply_eq_lintegral, MeasureTheory.measure_le_lintegral_pos, MeasureTheory.volume_sum_rpow_le, pi_map_eval, ProbabilityTheory.ae_cond_mem, MeasureTheory.ProbabilityMeasure.coeFn_def, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec, MeasureTheory.eventually_sub_right_iff, MeasureTheory.SimpleFunc.map_lintegral, notMem_support_iff, MeasureTheory.measure_le_setAverage_pos, MeasureTheory.ae_map_iff, MeasureTheory.Lp.coeFn_negPart_eq_max, MeasureTheory.Ico_ae_eq_Ioc, Real.volume_Ico, MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq, MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero, MeasureTheory.SimpleFunc.memLp_iff, ProbabilityTheory.IndepSet_iff, MeasureTheory.IsProbabilityMeasure.measure_univ, ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel, restrict_apply_eq_zero, ProbabilityTheory.Kernel.rnDeriv_toReal_pos, VitaliFamily.ae_tendsto_average_norm_sub, MeasureTheory.ae_neBot, MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ, OrthonormalBasis.volume_parallelepiped, MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq', MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable, MeasureTheory.laverage_mul_measure_univ, ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le, AddCircle.volume_closedBall, MeasureTheory.tendsto_measure_vadd_diff_isCompact_isClosed, NumberField.mixedEmbedding.realSpace.volume_eq_zero, MeasureDense.indicatorConstLp_subset_closure, ProbabilityTheory.preCDF_le_one, pi_Ico_ae_eq_pi_Icc, MeasureTheory.memLp_const_iff_enorm, MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, map_eq_sum, MeasureTheory.tendsto_smul_ae, AEMeasurable.ae_of_join, MeasureTheory.tendsto_measure_Iic_atTop, countable_meas_level_set_pos, ProbabilityTheory.Kernel.id_prod_apply', rnDeriv_smul_right_of_ne_top', pi_singleton, ProbabilityTheory.Kernel.condDistrib_trajMeasure, ae_eq_zero_of_integral_contDiff_smul_eq_zero, unitInterval.volume_Icc, MeasureTheory.tsum_measure_le_measure_univ, ProbabilityTheory.Kernel.eq_rnDeriv_measure, MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure, MeasureTheory.Martingale.eq_zero_of_predictable', ProbabilityTheory.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero, MeasureTheory.projectiveFamilyContent_congr, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero, MeasureTheory.measure_add_diff, IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul, everywherePosSubset_ae_eq, volume_regionBetween_eq_lintegral', MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, MeasureTheory.piContent_eq_measure_pi, restrict_iUnion_apply, DomMulAct.smul_aeeqFun_aeeq, restrict_apply_le, MeasureTheory.exists_null_frontier_thickening, InnerProductSpace.volume_ball, MeasureTheory.JordanDecomposition.exists_compl_positive_negative, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one, ProbabilityTheory.Kernel.ae_comp_iff, bind_apply_le, MeasureTheory.forall_measure_preimage_mul_iff, MeasureTheory.Supermartingale.le_zero_of_predictable', piecewise_ae_eq_restrict_compl, eventually_cofinite, ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le, MeasureTheory.condExp_indicator, HasOuterApproxClosed.measure_le_lintegral, MeasureTheory.setLIntegral_eq_zero_iff, MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf, ProbabilityTheory.bayesRisk_const_of_nonempty, add_apply, MeasureTheory.setLAverage_eq', MeasureTheory.dirac_eq_zero_iff_not_mem, rnDeriv_add, MeasureTheory.Ioo_ae_eq_Ico, ergodicSMul_iff, SchwartzMap.coeFn_toLp, ProbabilityTheory.cond_inter_self, MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn, aeconst_of_dense_aestabilizer_vadd, count_apply_lt_top, restrict_apply_univ, finset_sum_apply, MeasureTheory.AEEqFun.coeFn_mk, infinitePiNat_map_piCongrLeft, ProbabilityTheory.iCondIndepSets_singleton_iff, ProbabilityTheory.hasFiniteIntegral_compProd_iff', MeasureTheory.Ioc_ae_eq_Icc, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_measure_eq_zero, MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto, ProbabilityTheory.tilted_mul_apply_mgf', MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2, ProbabilityTheory.ae_cond_mem₀, MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero, PreErgodic.ae_empty_or_univ, MeasureTheory.tendsto_measure_iInter_le, tendsto_measure_thickening, ProbabilityTheory.bayesRisk_le_mul', comap_apply, addHaar_parallelepiped, MeasureTheory.lintegral_indicator_const_le, ProbabilityTheory.Kernel.ae_eq_of_compProd_eq, ProbabilityTheory.inter_pos_of_cond_ne_zero, MeasureTheory.smulInvariantMeasure_iff, setLIntegral_rnDeriv', ProbabilityTheory.iIndepSet.meas_biInter, ProbabilityTheory.uniformOn_eq_zero_iff, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', MeasureTheory.SimpleFunc.lintegral_eq_of_subset', MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, MeasureTheory.hausdorffMeasure_lineMap_image, aeconst_of_dense_setOf_preimage_vadd_eq, pi_univ, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, MeasureTheory.dirac_eq_one_iff_mem, MeasureTheory.le_measure_symmDiff, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf, MeasureTheory.ae_restrict_neBot, restrict_congr_meas, pi_Ioi_ae_eq_pi_Ici, MeasureTheory.measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite, MeasureTheory.ae_eq_restrict_biUnion_finset_iff, Set.OrdConnected.null_frontier, sum_apply₀, MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top, ProbabilityTheory.gaussianReal_apply, ProbabilityTheory.Kernel.densityProcess_fst_univ_ae, addHaarMeasure_apply, MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable, prod_prod, MeasureTheory.tilted_apply_eq_ofReal_integral, MeasureTheory.measure_lt_top_of_subset, ae_eq_zero_of_integral_smooth_smul_eq_zero, MeasureDense.fin_meas, MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, StieltjesFunction.measure_Ici, ProbabilityTheory.condExp_set_generateFrom_singleton, ProbabilityTheory.cond_eq_inv_mul_cond_mul, MeasureTheory.ae_dirac_iff, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero, MeasureTheory.measure_iUnion₀, MeasureTheory.measure_symmDiff_inv_smul, MeasureTheory.measure_vadd_eq_zero_iff, eq_rnDeriv₀, MeasurableSet.exists_isOpen_diff_lt, WeaklyRegular.innerRegular_measurable, Real.volume_pi_le_prod_diam, MeasureTheory.meas_ge_le_lintegral_div, MeasureTheory.Lp.coeFn_sup, ae_eq_or_eq_iff_eq_dirac_add_dirac, MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq, Set.Finite.measure_zero, ProbabilityTheory.condExp_generateFrom_singleton, measure_isAddHaarMeasure_eq_smul_of_isOpen, measure_eq_zero_of_subset_diff_everywherePosSubset, ProbabilityTheory.condDistrib_comp, MeasureTheory.AEEqFun.liftRel_iff_coeFn, MeasureTheory.condExp_smul, MeasureTheory.integrable_prod_iff, coe_add, ProbabilityTheory.meas_ge_le_variance_div_sq, MeasureTheory.lintegral_indicator_one₀, MeasureTheory.ae_eq_restrict_biUnion_iff, count_singleton, MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel, MeasureTheory.Submartingale.zero_le_of_predictable, MeasureTheory.setAverage_eq', IsAddFoelner.eventually_meas_ne_zero, MeasureTheory.measure_sigmaFiniteSetWRT', rnDeriv_add_right_of_mutuallySingular', InnerProductSpace.volume_ball_of_dim_odd, univ_pi_Ico_ae_eq_Icc, MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le, ProbabilityTheory.Kernel.comp_discard', ProbabilityTheory.monotone_preCDF, rnDeriv_ne_top, IsCompact.measure_eq_iInf_isOpen, ProbabilityTheory.Kernel.condExp_traj, MeasureTheory.measure_add_measure_compl, addHaarMeasure_self, MeasureTheory.measure_inter_inv_smul, MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure, MeasureTheory.measure_union₀_aux, measure_le_lintegral_thickenedIndicator, ae_smul_measure_iff, BoxIntegral.Box.volume_apply', ProbabilityTheory.Kernel.compProd_eq_zero_iff, Real.disjoint_residual_ae, ae_completion, MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq, MeasureTheory.SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero, MeasureTheory.measure_inter_lt_top_of_left_ne_top, pi_Ioo_ae_eq_pi_Icc, MeasureTheory.measure_neg_vadd_sdiff, MeasureTheory.ae_restrict_union_iff, MeasureTheory.mem_map_restrict_ae_iff, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, MeasureTheory.AEEqFun.smul_toGerm, comap_subtype_coe_apply, MeasureTheory.withDensity_eq_iff, ProbabilityTheory.condKernel_compProd, dimH_eq_iInf, tendsto_measure_Icc_nhdsWithin_right, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le, ProbabilityTheory.Kernel.rnDeriv_pos, sInf_apply, fst_apply, ProbabilityTheory.Kernel.density_ae_eq_limitProcess, MeasureTheory.smul_ae, MeasureTheory.integrable_conv_iff, measure_isMulInvariant_eq_smul_of_isCompact_closure, MeasureTheory.Integrable.to_average, inv_rnDeriv, ProbabilityTheory.IsRatCondKernelCDFAux.mono', Set.Countable.measure_zero, MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero, MeasureTheory.AEEqFun.coeFn_sup, MeasureTheory.ae_restrict_iff₀, ProbabilityTheory.strong_law_aux6, MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero, MeasureTheory.tendsto_sum_indicator_atTop_iff', ProbabilityTheory.Kernel.rnDerivAux_le_one, IsOpen.measure_eq_iSup_isCompact, MeasureTheory.lintegral_countable', MeasureTheory.tilted_const', MeasureTheory.SimpleFunc.integrable_iff, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, MeasureTheory.limsup_trim, fst_univ, Monotone.measure_iInter, MeasureTheory.ae_le_eLpNormEssSup, MeasureTheory.tendsto_measure_Ioc_atBot, univ_pi_Ioi_ae_eq_Ici, inf_apply, MeasureTheory.tilted_apply, measurable_measure_prodMk_left_finite, infinitePi_singleton_of_fintype, MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure, MeasureTheory.smul_le_stoppedValue_hitting, PMF.toMeasure_uniformOfFintype_apply, integrable_compProd_iff, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero, MeasureTheory.MeasurePreserving.measure_preimage_equiv, MeasureTheory.Integrable.condDistrib_ae, MeasureTheory.measure_eq_div_smul, AntilipschitzWith.le_hausdorffMeasure_image, Real.volume_Iic, MeasureTheory.rnDeriv_mconv, ProbabilityTheory.condIndepSets_iff, hausdorffMeasure_zero_or_top, ProbabilityTheory.setLIntegral_toKernel_univ, IsOpen.ae_eq_empty_iff_eq, MeasureTheory.log_rnDeriv_tilted_left_self, ProbabilityTheory.iCondIndepSet_iff, MeasureTheory.AEEqFun.coeFn_comp₂Measurable, ProbabilityTheory.uniformOn_eq_one_of, MeasureTheory.eLpNorm_indicator_const_le, MeasureTheory.condExp_add, ProbabilityTheory.condExpKernel_singleton_ae_eq_cond, isFoelner_iff, measure_toMeasurable_inter_of_cover, MeasureTheory.prob_compl_eq_zero_iff, MeasureTheory.exists_pos_ball, MeasureTheory.measure_union_add_inter₀', MeasureTheory.mem_ae_iff_prob_eq_one, MeasureTheory.ae_eq_dirac', ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul, MeasureTheory.measure_mul_laverage, MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.sum_measure_preimage_singleton, toSphere_apply', comap_apply₀, MeasureTheory.ae_eq_univ_iff_measure_eq, volume_subtype_coe_le_volume, Real.volume_Icc, ProbabilityTheory.condVar_ae_le_condExp_sq, ProbabilityTheory.IdentDistrib.measure_preimage_eq, compl_support_eq_sUnion, ProbabilityTheory.condDistrib_snd_prod, IsFoelner.tendsto_meas_smul_symmDiff_smul, MeasureTheory.AEEqFun.pow_toGerm, MeasureTheory.ae_eq_bot, DomAddAct.vadd_aeeqFun_aeeq, MeasureTheory.AEStronglyMeasurable.compProd_mk_left, MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter, MeasureTheory.vadd_mem_ae, ae_restrict_iff_subtype, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', ProbabilityTheory.IndepFun.meas_inter, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, MeasureTheory.boundedBy_measure, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint, MeasureTheory.AEEqFun.toGermMonoidHom_apply, ProbabilityTheory.Kernel.ext_iff', StieltjesFunction.measure_Ioi, coe_smul, le_liftLinear_apply, IsometryEquiv.hausdorffMeasure_preimage, MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq, DomAddAct.vadd_Lp_ae_eq, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm', MeasureTheory.measure_iUnion, AddAction.coe_aestabilizer, MeasureTheory.AEDisjoint.eq, MeasureTheory.measure_compl₀, MeasureTheory.FiniteMeasure.prod_apply, MeasureTheory.rnDeriv_mconv', measure_isAddInvariant_eq_smul_of_isCompact_closure, MeasurableEmbedding.gaussianReal_comap_apply, finiteAt_principal, sum_apply_eq_zero, Module.Basis.addHaar_eq_iff, MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc, Complex.volume_sum_rpow_lt, ProbabilityTheory.Kernel.IndepFun.meas_inter, ProbabilityTheory.IsRatCondKernelCDFAux.le_one', VitaliFamily.ae_tendsto_div, MeasureTheory.withDensity_eq_zero, MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null, VitaliFamily.ae_tendsto_measure_inter_div, MeasureTheory.measure_preimage_snd_singleton_eq_sum, MeasureTheory.SimpleFunc.const_lintegral, MeasureTheory.measure_lintegral_div_measure, MeasureTheory.ae_le_lpNorm_exponent_top, MeasureTheory.StronglyMeasurable.ae_le_trim_iff, IicSnd_apply, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, MeasureTheory.condExp_ae_eq_condExpL1CLM, measure_isHaarMeasure_eq_smul_of_isEverywherePos, measure_compl_support, ProbabilityTheory.iIndepSets.meas_biInter, BoundedContinuousFunction.coeFn_toLp, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, MeasureTheory.map_eq_setLIntegral_pdf, nnreal_smul_coe_apply, ProbabilityTheory.lintegral_toKernel_mem, MeasureTheory.indicatorConstLp_inj, ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self, Real.volume_pi_Ioo, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, addHaar_image_linearMap, MeasureTheory.measure_univ_of_isAddLeftInvariant, ae_ennreal_smul_measure_iff, MeasureTheory.tendsto_ae_condExp, MeasureTheory.eLpNorm_const', everywherePosSubset_ae_eq_of_measure_ne_top, MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant, ProbabilityTheory.cond_iInter, ProbabilityTheory.Kernel.parallelComp_apply', ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone, MeasureTheory.levyProkhorovEDist_le_max_measure_univ, ProbabilityTheory.uniformOn_self, MeasureTheory.ae_restrict_le, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, IsOpen.measure_eq_biSup_integral_continuous, MeasureTheory.ae_finsetSum_measure_iff, MeasureTheory.measure_map_restrict_apply, mem_support_iff_forall, MeasureTheory.AEEqFun.one_toGerm, MeasureTheory.IsFiniteMeasure.average, rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.measure_union_eq_top_iff, restrict_iUnion_apply_eq_iSup, FiniteSpanningSetsIn.finite, MeasureTheory.hausdorffMeasure_homothety_image, tendsto_ae_map, mutuallySingular_iff_disjoint_ae, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, ProbabilityTheory.Kernel.setLIntegral_density, MeasureTheory.integral_pos_iff_support_of_nonneg, ae_comp_iff, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup, MeasureTheory.setLIntegral_one, MeasureTheory.rnDeriv_ae_eq_condExp, MeasureTheory.withDensity_apply₀, VitaliFamily.ae_eventually_measure_zero_of_singular, Besicovitch.ae_tendsto_measure_inter_div, ergodicVAdd_iff, MeasureTheory.NoAtoms.measure_singleton, one_le_hausdorffMeasure_zero_of_nonempty, Real.volume_pi_Ioo_toReal, rnDeriv_pos, coe_finset_sum, smul_measure_isMulInvariant_le_of_isCompact_closure, ProbabilityTheory.hasFiniteIntegral_comp_iff', ProbabilityTheory.cond_add_cond_compl_eq, MeasureTheory.measure_diff_add_inter, MeasureTheory.ae_restrict_biUnion_finset_iff, MeasureTheory.pdf.IsUniform.pdf_eq, MeasureTheory.Integrable.measure_norm_gt_lt_top, lintegral_condKernel_mem, measure_isAddHaarMeasure_eq_smul_of_isEverywherePos, MeasureTheory.measure_toMeasurable, MeasureTheory.sub_nonneg_ae, countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top, MeasureTheory.Integrable.ae_convolution_exists, MeasureTheory.AEStronglyMeasurable.ae_of_compProd, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero, MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc, count_apply_finset', exists_sum_smul_dirac, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀, measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable, ProbabilityTheory.condExpKernel_ae_eq_condExp, MeasureTheory.one_le_prob_iff, LipschitzWith.ae_differentiableAt, VitaliFamily.ae_tendsto_lintegral_div', MutuallySingular.measure_nullSet, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf', ProbabilityTheory.hasFiniteIntegral_comp_iff, MeasureTheory.hausdorffMeasure_vadd, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel, InnerRegularCompactLTTop.innerRegular, MeasureTheory.AEEqFun.coeFn_compMeasurable, pi_Ioo_ae_eq_pi_Ioc, MeasureTheory.union_ae_eq_right_iff_ae_subset, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, addHaar_affineSubspace, MeasureTheory.Lp.simpleFunc.coeFn_le, measure_Icc_lt_top, MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf, Real.volume_Ioc, dirac_apply_ne_zero_iff_eq_one, Metric.measure_closedEBall_pos, ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_mutuallySingularSetSlice, MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac, ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul, MeasureTheory.condLExp_smul_le, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, EuclideanSpace.volume_ball_fin_three, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, Convex.addHaar_frontier, QuasiMeasurePreserving.ae_map_le, MeasureTheory.AddSubgroup.index_mul_measure, ProbabilityTheory.Kernel.compProd_apply_univ_le, intervalIntegrable_const_iff, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, addHaar_image_continuousLinearEquiv, hausdorffMeasure_le_liminf_tsum, MeasureTheory.setLAverage_eq, le_map_apply, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm, MeasureTheory.condExp_of_aestronglyMeasurable', ProbabilityTheory.Kernel.lintegral_density, MeasureTheory.isClosed_setOf_preimage_ae_eq, notMem_support_iff_exists, MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp, MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant, MeasureTheory.lintegral_finset, Complex.volume_closedBall, MeasureTheory.Lp.coeFn_nonneg, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, ae_le_iff_absolutelyContinuous, MeasureTheory.ae_eq_dirac, ProbabilityTheory.cond_mul_eq_inter', MeasureTheory.measure_inter_add_diff, MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt, MeasureTheory.nnnorm_indicatorConstLp_le, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const, ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, ProbabilityTheory.Kernel.measurable_densityProcess_aux, measure_preimage_of_map_eq_self, dirac_apply_eq_zero_or_one, ProbabilityTheory.integrable_compProd_iff, pi_closedBall, MeasureTheory.vadd_set_ae_eq, MeasureTheory.ae_restrict_biUnion_finset_eq, MeasureTheory.toMeasurable_def, MeasureTheory.Supermartingale.condExp_ae_le, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const, MeasureTheory.integral_le_measure, HasOuterApproxClosed.tendsto_lintegral_apprSeq, MeasureTheory.Lp.coeFn_lpSMul, VitaliFamily.covering, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum, MeasureTheory.Lp.simpleFunc.coeFn_zero, MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc, MeasureTheory.measure_preimage_smul_of_nullMeasurableSet, ProbabilityTheory.iCondIndepSets_iff, sub_apply, MeasureTheory.lintegral_singleton', QuasiMeasurePreserving.tendsto_ae, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, MeasureTheory.condExpIndSMul_nonneg, MeasureTheory.measure_add_measure_eq, MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm, MeasureTheory.exp_neg_llr, Real.volume_eball, ProbabilityTheory.iIndep_iff, MeasureTheory.lintegral_unique, MeasureTheory.ae_restrict_eq, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, dirac_apply_ne_one_iff_eq_zero, inv_apply, MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq, ProbabilityTheory.IsRatCondKernelCDFAux.iInf_rat_gt_eq, Bornology.IsBounded.measure_lt_top, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀, ProbabilityTheory.Kernel.prodMkLeft_apply', MeasureTheory.exp_neg_llr', Real.volume_le_diam, MeasureTheory.le_toMeasure_apply, MeasureTheory.condExp_smul_of_aestronglyMeasurable_left, MeasurableEmbedding.comap_apply, rnDeriv_singularPart, MeasureTheory.measure_add_closure_zero, MeasureTheory.ofReal_setIntegral_one, MeasureTheory.AEEqFun.coeFn_add, ContinuousLinearMap.coeFn_compLpL, NumberField.mixedEmbedding.volume_negAt_plusPart, MeasureTheory.insert_ae_eq_self, NumberField.mixedEmbedding.convexBodyLT'_volume, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, MeasureTheory.sum_measure_le_measure_univ, MeasureTheory.mem_ae_iff_prob_eq_one₀, support_mem_ae, LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real, ProbabilityTheory.IsRatCondKernelCDFAux.le_one, ae_restrict_le_codiscreteWithin, ProbabilityTheory.uniformOn_add_compl_eq, ENNReal.count_const_le_le_of_tsum_le, dirac_apply_of_mem, MeasureTheory.IsProjectiveLimit.measure_cylinder, MeasureTheory.condLExp_bot_ae_eq, MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq, MeasureTheory.diracProba_toMeasure_apply', MeasureTheory.tendsto_vadd_ae, ProbabilityTheory.measure_stieltjesOfMeasurableRat_univ, essInf_eq_sSup, Isometry.hausdorffMeasure_preimage, MeasureTheory.toMeasure_apply₀, ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi, MeasureTheory.SignedMeasure.rnDeriv_smul, MeasureTheory.le_trim, MeasureTheory.hausdorffMeasure_smul_right_image, MeasureTheory.SimpleFunc.measure_support_lt_top_of_lintegral_ne_top, ProbabilityTheory.Kernel.rnDeriv_lt_top, compProd_apply_prod, MeasureTheory.rnDeriv_tilted_left, MeasureTheory.pdf_of_not_aemeasurable, count_apply_infinite, compl_mem_cofinite, StieltjesFunction.measure_Icc, ProbabilityTheory.Kernel.fst_apply', MulAction.coe_aestabilizer, MeasureTheory.isProbabilityMeasure_iff, MeasureTheory.trim_measurableSet_eq, ZLattice.volume_image_eq_volume_div_covolume, measurable_measure_prodMk_left, MeasureTheory.IsFundamentalDomain.measure_eq_tsum', MeasureTheory.setLIntegral_const, ae_eq_of_integral_contMDiff_smul_eq, measure_toMeasurable_inter_of_sum, MeasureTheory.smul_mem_ae, AbsolutelyContinuous.ae_le, comap_apply_le, indicator_ae_eq_restrict_compl, MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant, MeasureTheory.measure_inv_smul_symmDiff, ProbabilityTheory.Kernel.iIndep.meas_iInter, MeasureTheory.ae_restrict_uIoc_iff, cofinite_le_ae, measure_isAddLeftInvariant_eq_vadd_of_ne_top, MeasureTheory.mul_meas_ge_le_lintegral₀, MeasureTheory.Submartingale.zero_le_of_predictable', ProbabilityTheory.posterior_boolKernel_apply_false, ProbabilityTheory.Kernel.singularPart_of_subset_compl_mutuallySingularSetSlice, addHaar_smul_of_nonneg, MeasureTheory.condExpIndL1Fin_disjoint_union, measure_neg, Set.Subsingleton.measure_zero, rnDeriv_withDensity, LipschitzOnWith.ae_differentiableWithinAt_real, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, MeasureTheory.MeasurePreserving.aeconst_preimage, ProbabilityTheory.setLIntegral_toKernel_prod, MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux, Finset.measure_zero, MeasurableEmbedding.map_apply, snd_univ, ProbabilityTheory.Fernique.measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self, MeasureTheory.laverage_union, VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt, MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero, MeasureTheory.tendsto_measure_iInter_atTop, MeasureTheory.tendsto_measure_Ici_atBot, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp, MeasureTheory.lintegral_indicator_const, ext_prod₃_iff, Subtype.volume_univ, Besicovitch.exists_disjoint_closedBall_covering_ae, MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, ProbabilityTheory.Kernel.snd_apply', MeasureTheory.AECover.ae_tendsto_indicator, MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le, MeasureTheory.measure_eq_iInf', MeasureTheory.volume_pi_ball, finite_const_le_meas_of_disjoint_iUnion₀, ae_count_iff, MeasureTheory.AEEqFun.comp₂_toGerm, MeasureTheory.AEEqFun.sub_toGerm, measure_eq_measure_preimage_add_measure_tsum_Ico_zpow, count_apply_finset, MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl, MeasureTheory.inv_measure_univ_smul_eq_self, IsCompact.measure_lt_top, MeasureTheory.measure_if, ProbabilityTheory.measurable_condExpKernel, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, MeasureTheory.Ioo_ae_eq_Ioc, EMetric.measure_ball_pos, map_apply_of_aemeasurable, MeasureTheory.measure_smul, MeasureTheory.ae_mem_iff_measure_eq, MeasureTheory.FiniteMeasure.mk_apply, iInf_rat_gt_prod_Iic, ProbabilityTheory.condDistrib_self, ProbabilityTheory.strong_law_aux7, MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim, MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed, MeasureTheory.integrable_prod_iff', addHaar_closedBall_mul_of_pos, MeasureTheory.not_isFiniteMeasure_iff, PMF.toMeasure_apply_eq_one_iff, liftLinear_apply, ProbabilityTheory.uniformOn_inter_self, MeasureTheory.measure_inv_smul_union, ProbabilityTheory.Kernel.compProd_preimage_fst, MeasureTheory.MeasurePreserving.aeconst_comp, measure_zero_of_dimH_lt, mem_support_restrict, ProbabilityTheory.condExp_ae_eq_integral_condDistrib', IsUnifLocDoublingMeasure.ae_tendsto_average, ProbabilityTheory.Kernel.condExp_densityProcess, EuclideanSpace.volume_ball_fin_two, MeasureTheory.MeasurePreserving.measure_preimage_le, MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp, ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess, NumberField.mixedEmbedding.volume_eq_zero, IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub, count_univ, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', MeasureTheory.map_mul_right_ae, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder, MeasureTheory.ae_lt_top', MeasureTheory.SimpleFunc.eLpNorm'_eq, MeasureTheory.measure_union₀', le_iff, MeasureTheory.indicatorConstLp_coeFn_notMem, NNRealRMK.le_rieszMeasure_of_tsupport_subset, MeasureTheory.measure_le_eq_lt, RealRMK.exists_open_approx, ProbabilityTheory.tilted_mul_apply_mgf, ProbabilityTheory.Kernel.prodMkRight_apply', EuclideanSpace.volume_ball, ProbabilityTheory.bayesRisk_le_iInf', real_def, MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero, unitInterval.volume_Ioc, MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds, MeasureTheory.Martingale.condExp_ae_eq, ContinuousMap.coeFn_toLp, MeasureTheory.AEEqFun.coeFn_star, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, AddCircle.addWellApproximable_ae_empty_or_univ, MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq, MeasureTheory.setLIntegral_pdf_le_map, MeasureTheory.ae_dirac_eq, Metric.measure_eball_pos, MeasureTheory.AECover.ae_eventually_mem, MeasureTheory.measure_preimage_smul_le, measure_mono_left, MeasureTheory.AEEqFun.coeFn_zero, MeasureTheory.measure_lintegral_sub_measure, MeasureTheory.mulEquivHaarChar_smul_preimage, addHaar_preimage_linearMap, Metric.measure_closedBall_pos, Real.volume_Ici, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq, MeasureTheory.AEEqFun.toGermAddMonoidHom_apply, measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.measure_preimage_vadd_le, MeasureTheory.mul_meas_ge_le_lintegral, MeasureTheory.volume_pi_closedBall, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real, measure_pos_of_nonempty_interior, MeasureTheory.measure_union_toMeasurable, ProbabilityTheory.condDistrib_comp_self, MeasureTheory.measure_biUnion_finset₀, MeasureTheory.lpTrimToLpMeas_ae_eq, Antitone.measure_iInter, Real.volume_uIoo, MeasureTheory.eventually_nhds_one_measure_smul_diff_lt, MeasureTheory.rnDeriv_conv', MeasureTheory.AEEqFun.coeFn_compMeasurePreserving, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, measurable_measure_prodMk_right, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv, MeasureTheory.exists_subordinate_pairwise_disjoint, MeasureTheory.exists_measurable_superset_iff_measure_eq_zero, ZLattice.volume_image_eq_volume_div_covolume', InnerRegularWRT.measure_eq_iSup, addHaar_preimage_continuousLinearEquiv, MeasureTheory.measure_biUnion_finset, VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous, countable_meas_pos_of_disjoint_iUnion, MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume, ProbabilityTheory.bayesRisk_const_of_neZero, ProbabilityTheory.iCondIndepFun_iff, addHaar_ball_mul_of_pos, ProbabilityTheory.HasCondSubgaussianMGF.cgf_le, MeasureTheory.pdf.lintegral_eq_measure_univ, MeasureTheory.IsAddFundamentalDomain.ae_covers, tendsto_measure_cthickening_of_isClosed, MeasureTheory.measure_eq_iInf, MeasureTheory.MemLp.meas_ge_lt_top', Real.volume_pi_Ico_toReal, ProbabilityTheory.uniformOn_univ, iSup_restrict_spanningSets, MeasureTheory.tendsto_measure_iInter_atBot, MeasureTheory.ae_mem_limsup_atTop_iff, MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal, ProbabilityTheory.Kernel.compProd_apply_univ, MeasureTheory.lintegral_fintype, apply_eq_zero_of_isEmpty, MeasureTheory.setLIntegral_eq_zero_iff', univ_pi_Iio_ae_eq_Iic, measure_Ioo_eq_zero, exists_positive_of_not_mutuallySingular, MeasureTheory.tsum_measure_preimage_singleton, MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, MeasureTheory.AEEqFun.coeFn_inv, Real.volume_pi_le_diam_pow, ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic, restrict_apply₀, MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem, addHaar_nnreal_smul, MeasureTheory.measure_diff, MeasureTheory.neg_ae, ProbabilityTheory.uniformOn_inter', ProbabilityTheory.Kernel.deterministic_apply', measure_Ioo_lt_top, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group, MeasureTheory.martingalePart_add_ae_eq, MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq, MeasureTheory.measure_eq_sub_vadd, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg, addHaar_submodule, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, VitaliFamily.ae_tendsto_rnDeriv, DomMulAct.smul_Lp_ae_eq, MeasureTheory.measure_inter_neg_vadd, IsCompact.exists_open_superset_measure_lt_top, FiniteAtFilter.inf_ae_iff, addHaar_singleton_add_smul_div_singleton_add_smul, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, MeasureTheory.AEEqFun.div_toGerm, PMF.toMeasure_apply_eq_of_inter_support_eq, ProbabilityTheory.iIndepSet_iff, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum', MeasureTheory.measure_add_lintegral_eq, MeasureTheory.measure_diff', ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone, MeasureTheory.ae_const_le_iff_forall_lt_measure_zero, MeasureTheory.AEDisjoint.exists_disjoint_diff, ProbabilityTheory.Kernel.borelMarkovFromReal_apply, MeasureTheory.measure_toMeasurable_union, MeasureTheory.MeasuredSets.continuous_measure, FiniteAtFilter.eventually, Set.exists_isOpen_le_add, ProbabilityTheory.strong_law_aux4, ProbabilityTheory.Kernel.measure_le_bound, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop, ProbabilityTheory.condVar_neg, ProbabilityTheory.Kernel.lintegral_rnDeriv, le_map_apply_image, ProbabilityTheory.Kernel.integrable_traj, PreErgodic.prob_eq_zero_or_one, MeasureTheory.FiniteMeasure.prod_apply_symm, MeasureTheory.Integrable.coeFn_toL1, smul_apply, MeasureTheory.measure_inv_smul_inter, MeasureTheory.average_eq', MeasureTheory.sum_measure_singleton, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd', ProbabilityTheory.uniformOn_union, ae_measure_lt_top, ProbabilityTheory.condVar_bot_ae_eq, inv_rnDeriv_aux, MeasureTheory.tendstoInMeasure_ae_unique, MeasureTheory.tilted_zero', MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_le, LipschitzWith.ae_differentiableAt_of_real, MeasureTheory.Submartingale.ae_tendsto_limitProcess, MeasureTheory.measure_union_neg_vadd, MeasureTheory.ae_eq_of_setLIntegral_prod_eq, MeasurableEmbedding.comap_preimage, le_count_apply, integrable_comp_iff, MeasureTheory.FiniteMeasure.coeFn_mk, instNeZeroENNRealCoeSetUniv, MeasureTheory.ProbabilityMeasure.mk_apply, ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.ProbabilityMeasure.map_apply', MeasureTheory.condExp_restrict_ae_eq_restrict, ProbabilityTheory.iIndepFun.meas_iInter, hausdorffMeasure_of_dimH_lt, MeasureTheory.smul_set_ae_eq, ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot, MeasureTheory.UnifTight.exists_measurableSet_indicator, ProbabilityTheory.Kernel.setLIntegral_rnDeriv, MeasureTheory.hasFiniteIntegral_prod_iff, MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq, MeasureTheory.exists_null_frontiers_thickening, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, absolutelyContinuous_compProd_iff', MutuallySingular.measure_compl_nullSet, restrict_iUnion_apply_ae, MeasureTheory.pdf.eq_of_map_eq_withDensity', tendsto_IicSnd_atTop, MeasureTheory.Lp.coeFn_negPart, MeasureTheory.isZeroOrProbabilityMeasure_iff, MeasureTheory.Integrable.prod_left_ae, MeasureTheory.integrableOn_singleton_iff, ae_smul_measure_le, MeasureTheory.SimpleFunc.lintegral_eq_of_subset, ProbabilityTheory.condVar_of_aestronglyMeasurable, ProbabilityTheory.IsSetBernoulli.ae_subset, measure_Ioo_pos, MeasureTheory.measure_ball_lt_top, support_eq_sInter, MeasureTheory.measure_sUnion₀, ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae, MeasureTheory.measure_symmDiff_eq, StieltjesFunction.measure_Ioc, rnDeriv_withDensity₀, MeasureTheory.eLpNorm_indicator_const', MeasureTheory.AEEqFun.coeFn_posPart, IsUpperSet.null_frontier, MeasureTheory.ae_restrict_iff, MeasureTheory.llr_tilted_left, infinitePi_cylinder, MeasureTheory.projectiveFamilyFun_congr, MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_withDensity_iff', MeasureTheory.lintegral_le_meas, ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod, MeasureTheory.eLpNorm'_eq_zero_iff, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le, MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd, MeasureTheory.measure_le_integral_pos, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf, MutuallySingular.disjoint_ae, ProbabilityTheory.posterior_id, MeasureTheory.FiniteMeasure.map_apply', MeasureTheory.measure_union, MeasureTheory.lintegral_insert, hausdorffMeasure_apply, MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero, Ergodic.mem_extremePoints_measure_univ_eq, MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt, map_const, ProbabilityTheory.Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self, MeasureTheory.Submartingale.upcrossings_ae_lt_top', MeasureTheory.maximal_ineq, MeasureTheory.AEEqFun.mk_toGerm, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg', MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder, MeasureTheory.distribHaarChar_eq_div, blimsup_cthickening_ae_eq_blimsup_thickening, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.IsProbabilityMeasure.ae_neBot, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure, count_apply_finite', tendsto_measure_Icc_nhdsWithin_right', sub_apply_eq_zero_of_isHahnDecomposition, measure_Ico_lt_top, dirac_apply, MeasureTheory.exists_measurable_superset_forall_eq, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, ProbabilityTheory.cond_eq_zero, MeasureTheory.lintegral_indicator_one, ProbabilityTheory.meas_ge_le_evariance_div_sq, MeasureTheory.exists_setLIntegral_compl_lt, MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier, MeasureTheory.diracProba_toMeasure_apply, MeasureTheory.ae_restrict_iff', NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, completion_apply, le_join_apply, MeasureTheory.measure_preimage_smul, ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice, rnDeriv_smul_left, MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant, MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator, MeasureTheory.hausdorffMeasure_smul, restrict_apply_eq_zero', MeasureTheory.pow_mul_meas_ge_le_eLpNorm, exists_measure_inter_spanningSets_pos, VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous, Set.measure_eq_iInf_isOpen, MeasureTheory.eLpNorm_const, mkMetric_le_liminf_sum, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice, MeasureDense.nonempty', ProbabilityTheory.Kernel.comapRight_apply', MeasureTheory.null_iff_of_isAddLeftInvariant, curveIntegralFun_trans_aeeq_left, piecewise_ae_eq_restrict, ProbabilityTheory.Kernel.eLpNorm_density_le, polarCoord_source_ae_eq_univ, ProbabilityTheory.cond_apply', MeasureTheory.distribHaarChar_mul, addHaar_preimage_linearEquiv, hausdorffMeasure_le_one_of_subsingleton, MeasureTheory.measure_eq_inducedOuterMeasure, IsAddFoelner.tendsto_nhds_mean, MeasureTheory.pdf.IsUniform.integral_eq, LipschitzOnWith.hausdorffMeasure_image_le, MeasureTheory.hausdorffMeasure_affineSegment, IsCompact.measure_eq_biInf_integral_hasCompactSupport, rnDeriv_restrict_self, MeasureTheory.Lp.coeFn_zero, Complex.volume_ball, MeasureTheory.toMeasure_apply, ProbabilityTheory.ae_cond_of_forall_mem, ProbabilityTheory.iIndepSet_iff_meas_biInter, StieltjesFunction.measure_Iio, MeasureTheory.measureReal_def, ae_integrable_of_integrable_comp, StieltjesFunction.ae_hasDerivAt, MeasureTheory.le_ae_restrict, ProbabilityTheory.strong_law_aux1, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot, ProbabilityTheory.measure_condCDF_Iic, MeasureTheory.AEEqFun.mk_eq_mk, ProbabilityTheory.indepSet_iff_measure_inter_eq_mul, MeasurableEmbedding.ae_map_iff, MeasureTheory.measure_symmDiff_neg_vadd, MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ, MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior, IsCompact.measure_lt_top_of_nhdsWithin, PMF.toMeasure_bindOnSupport_apply, ProbabilityTheory.Kernel.densityProcess_fst_univ, MeasureTheory.tendsto_measure_iUnion_accumulate, MeasureTheory.Integrable.measure_le_lt_top, MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul, rnDeriv_withDensity_left_of_absolutelyContinuous, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀, MeasureTheory.lintegral_pos_iff_support, aestronglyMeasurable_iff_nullMeasurable_separable, MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure, LipschitzWith.coeFn_compLp, ProbabilityTheory.hasFiniteIntegral_compProd_iff, ae_mono', ProbabilityTheory.strong_law_ae_simpleFunc_comp, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le, MeasureTheory.IsProjectiveLimit.measure_univ_unique, MeasureTheory.SignedMeasure.rnDeriv_neg, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, ProbabilityTheory.IndepFun_iff, addHaar_closedBall, MeasureTheory.OuterMeasure.coe_mkMetric, MeasureTheory.submartingale_iff_condExp_sub_nonneg, MeasureTheory.Lp.coeFn_neg, tendsto_measure_cthickening_of_isCompact, MeasureTheory.condExp_bilin_of_stronglyMeasurable_right, MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact, MeasureTheory.measure_preimage_eq_zero_iff_of_countable, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const, MeasureTheory.Lp.coeFn_abs, VitaliFamily.ae_eventually_measure_pos, ProbabilityTheory.posterior_posterior, MeasureTheory.eLpNorm_indicator_const₀, MeasureTheory.AEEqFun.mul_toGerm, PMF.toMeasure_apply_inter_support, infinitePi_singleton, MeasureTheory.isZeroOrProbabilityMeasureSMul, ProbabilityTheory.lintegral_preCDF_fst, coe_completion, VitaliFamily.measure_limRatioMeas_top, Monotone.measure_iUnion, MeasureTheory.measure_preimage_add_right, MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range, ProbabilityTheory.condDistrib_const, ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop, dirac_compProd_apply, MeasureTheory.AEEqFun.zpow_toGerm, MeasureTheory.AEEqFun.comp_toGerm, MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀, measure_prod_null, ProbabilityTheory.evariance_eq_zero_iff, AlternatingMap.measure_parallelepiped, blimsup_thickening_mul_ae_eq, ProbabilityTheory.Kernel.iIndepFun.meas_iInter, count_apply_eq_top', ext_iff_singleton, Real.volume_univ, measure_support_eq_zero_iff, finite_const_le_meas_of_disjoint_iUnion, MeasureTheory.eventually_add_left_iff, MeasureTheory.countable_meas_le_ne_meas_lt, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet, MeasureTheory.exp_llr_of_ac, IsAddFoelner.tendsto_meas_vadd_symmDiff, measure_pos_of_mem_nhds, MeasureTheory.ae_eq_condLExp₀, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, MeasureTheory.Lp.coeFn_sub, ProbabilityTheory.strong_law_aux2, MeasureTheory.eventually_mul_right_iff, MeasureTheory.AEEqFun.coeFn_zpow, MeasureTheory.measure_add_measure_compl₀, MeasureTheory.condLExp_smul', ProbabilityTheory.uniformOn_compl, MeasureTheory.tendstoInMeasure_iff_enorm, ProbabilityTheory.condDistrib_fst_prod, MeasureTheory.Lp.meas_ge_le_mul_pow_enorm, IsClosed.measure_eq_univ_iff_eq, measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, MeasureTheory.measure_average_le_pos, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one, join_apply, tsum_indicator_apply_singleton, LipschitzWith.hausdorffMeasure_image_le, MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt, volume_regionBetween_eq_integral, mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem, ContinuousLinearMap.coeFn_compLp, ProbabilityTheory.setLIntegral_condCDF, MeasureTheory.measure_setAverage_le_pos, MeasureTheory.withDensity_apply', MeasurableSet.exists_isCompact_isClosed_lt_add, ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self, ProbabilityTheory.Kernel.pow_succ_apply_eq_lintegral, ProbabilityTheory.Kernel.iIndepFun.meas_biInter, ProbabilityTheory.Kernel.IndepFun.measure_inter_preimage_eq_mul, MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant', MeasureTheory.AEDisjoint.diff_ae_eq_left, ProbabilityTheory.posterior_eq_withDensity_of_countable, ProbabilityTheory.IsFiniteKernel.exists_univ_le, MeasureTheory.lintegral_nnnorm_condExpIndSMul_le, ProbabilityTheory.avgRisk_const_right', MeasureTheory.measure_le_average_pos, volume_preimage_coe, ProbabilityTheory.iIndep.meas_iInter, ae_not_liouville, ProbabilityTheory.measure_condCDF_univ, ProbabilityTheory.lintegral_stieltjesOfMeasurableRat, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.AEDisjoint.measure_diff_right, MeasureTheory.measure_eq_trim, MeasureTheory.AEEqFun.zero_toGerm, InnerProductSpace.volume_closedBall, compProd_eq_zero_iff, MeasureTheory.measure_preimage_vadd, Directed.measure_iInter, MeasureTheory.eLpNorm_const_lt_top_iff, IicSnd_univ, measure_Ioc_lt_top, le_dirac_apply, volumeIoiPow_apply_Iio, countable_meas_level_set_pos₀, ProbabilityTheory.Kernel.comp_apply', MeasureTheory.Martingale.ae_eq_condExp_limitProcess, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero, MeasureTheory.prob_compl_eq_one_sub, MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv, MeasureTheory.null_iff_of_isMulLeftInvariant, ProbabilityTheory.strong_law_ae_real, MeasureTheory.ae_restrict_iff'₀, ProbabilityTheory.IdentDistrib.measure_mem_eq, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2, exists_null_set_measure_lt_of_disjoint, MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier, MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed, InnerProductSpace.volume_closedBall_of_dim_odd, ProbabilityTheory.strong_law_aux5, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, StieltjesFunction.measure_Ico, MeasureTheory.FiniteMeasure.ennreal_mass, ProbabilityTheory.uniformOn_singleton, MeasureTheory.Lp.coeFn_posPart, MutuallySingular.rnDeriv_ae_eq_zero, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, pi_polarCoord_symm_target_ae_eq_univ, toSphereBallBound_mul_measure_unitBall_le_toSphere_ball, ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae, count_apply_lt_top', MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt, tendsto_eval_ae_ae, MeasureTheory.AEEqFun.coeFn_pow, BoxIntegral.unitPartition.volume_box, measure_univ_eq_zero, MeasureTheory.measure_mul_lintegral_eq, addHaar_closedBall_mul, Complex.volume_sum_rpow_lt_one, tendsto_IicSnd_atBot, MeasureTheory.IsFundamentalDomain.measure_eq, MeasureTheory.eLpNormEssSup_eq_zero_iff, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero', measure_Ioi_pos, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, MeasureTheory.measure_iUnion_eq_iSup_accumulate, ProbabilityTheory.setBernoulli_ae_subset, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite', AddAction.aeconst_of_aestabilizer_eq_top, MeasureTheory.measure_neg_vadd_union, pi_empty_univ, IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero, ProbabilityTheory.condDistrib_map, ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet, blimsup_cthickening_mul_ae_eq, measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet, ext_iff', ProbabilityTheory.Kernel.eq_rnDeriv, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite, ProbabilityTheory.Kernel.compProd_eq_iff, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq, MeasureTheory.llr_smul_right, ProbabilityTheory.Kernel.compProd_apply, ae.neBot, IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero, MeasureTheory.condExp_indep_eq, MeasurableEquiv.gaussianReal_map_symm_apply, ProbabilityTheory.IndepSets_iff, MeasureTheory.FinStronglyMeasurable.fin_support_approx, ProbabilityTheory.cond_mul_eq_inter, MeasureTheory.ae_map_mem_range, ProbabilityTheory.IsCondKernelCDF.lintegral, sigmaFinite_iff_measure_singleton_lt_top, MeasureTheory.ae_le_of_forall_setIntegral_le, ProbabilityTheory.Kernel.withDensity_apply', ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_aestronglyMeasurable, rnDeriv_withDensity_rnDeriv, MeasureTheory.toFinite_apply_eq_zero_iff, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.measure_sUnion, MeasureTheory.AEStronglyMeasurable.prodMk_left, MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm, count_apply_finite, addHaar_ball, AEMeasurable.ae_mem_imp_eq_mk, MeasureTheory.eLpNorm_sub_le_of_dist_bdd, MeasureTheory.integrable_average, MeasureTheory.laverage_add_measure, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac, MeasureTheory.measure_eq_extend, StieltjesFunction.measure_Iic, map_apply₀, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, exists_ae_subset_biUnion_countable, ProbabilityTheory.Kernel.rnDeriv_add, AEMeasurable.ae_eq_mk, ProbabilityTheory.setLIntegral_preimage_condDistrib, tprod_tprod, Besicovitch.exists_disjoint_closedBall_covering_ae_aux, AddCircle.closedBall_ae_eq_ball, MeasureTheory.measure_union', IntervalIntegrable.ae_hasDerivAt_integral, ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd, MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero, AddAction.mem_aestabilizer, MeasureTheory.rnDeriv_tilted_right, MeasureTheory.exists_measurable_superset, MeasureTheory.eventuallyConst_neg_set_ae, ProbabilityTheory.Kernel.sum_apply', ae_compProd_iff, ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul, Real.volume_uIoc, MeasureTheory.smul_set_ae_le, MeasureTheory.measure_setLAverage_le_pos, ae_eq_restrict_iff_indicator_ae_eq, ProbabilityTheory.strong_law_ae_of_measurable, MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero, absolutelyContinuous_compProd_right_iff, MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, snd_apply, unitInterval.volume_uIoc, MeasureTheory.condExp_sub, ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure, MeasureTheory.condExpIndSMul_ae_eq_smul, PreErgodic.ae_mem_or_ae_notMem, ae_pi_le_pi, addHaar_closedBall_center, MeasureTheory.Lp.dense_hasCompactSupport_contDiff, Real.volume_Ioi, ProbabilityTheory.Kernel.swapLeft_apply', toENNRealVectorMeasure_apply_measurable, MeasureTheory.IsFundamentalDomain.ae_covers, ProbabilityTheory.condIndepFun_iff, rnDeriv_self, MeasureTheory.lpMeas.ae_fin_strongly_measurable', Real.volume_Ioo, MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null, MeasureTheory.prob_add_prob_compl, Metric.measure_ball_pos, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, MeasureTheory.ProbabilityMeasure.prod_apply_symm, ProbabilityTheory.lintegral_condKernel_mem, ProbabilityTheory.IndepSet.measure_inter_eq_mul, MeasureTheory.measure_preimage_mul_right, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, VitaliFamily.ae_tendsto_limRatioMeas, ProbabilityTheory.Kernel.rnDeriv_self, IsAntichain.volume_eq_zero, ProbabilityTheory.Kernel.measurable_kernel_prodMk_right, MeasureTheory.AEEqFun.compMeasurePreserving_toGerm, MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, MeasurableSet.exists_isOpen_symmDiff_lt, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range, MeasureTheory.hausdorffMeasure_homothety_preimage, restrict_apply', MeasureTheory.eventually_add_right_iff, MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd, IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero', pi_Iio_ae_eq_pi_Iic, ProbabilityTheory.gaussianReal_apply_eq_integral, MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le, ENNReal.ae_eq_zero_of_lintegral_rpow_eq_zero, MeasureTheory.measure_union_add_inter₀, ProbabilityTheory.IsRatCondKernelCDF.mono, VitaliFamily.eventually_measure_lt_top, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self, ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff, VitaliFamily.ae_tendsto_average, RealRMK.le_rieszMeasure_tsupport_subset, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq, NumberField.mixedEmbedding.convexBodySum_volume, MeasureTheory.ae_restrict_iUnion_iff, MeasureTheory.SimpleFunc.finMeasSupp_iff, indicator_ae_eq_restrict, MeasureTheory.le_measure_diff, ProbabilityTheory.Kernel.comp_apply_univ_le, MeasureTheory.Lp.coeFn_inf, MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn, IsLowerSet.null_frontier, volume_image_subtype_coe, ProbabilityTheory.uniformOn_disjoint_union, ofMeasurable_apply, MeasureTheory.tilted_apply_eq_ofReal_integral', MeasureTheory.measure_le_measure_union_right, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_univ_le_one, MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq, MeasureTheory.measure_add_right_null, MeasureTheory.tendsto_measure_Ico_atTop, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le_exp_add, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀, MeasureTheory.eventuallyConst_vadd_set_ae, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall, FiniteAtFilter.exists_mem_basis, ProbabilityTheory.condKernel_const, rnDeriv_add', MeasurableSet.exists_isClosed_diff_lt, measure_preimage_inv, pi_pi, setLIntegral_rnDeriv_le, MeasureTheory.AEEqFun.coeFn_div, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup, MeasureTheory.Integrable.condDistrib_ae_map, MeasureTheory.integrable_mconv_iff, restrict_apply₀', ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib', MeasureTheory.ProbabilityMeasure.coeFn_mk, MeasureTheory.rnDeriv_tilted_left_self, MeasureTheory.measure_eq_top_of_lintegral_ne_top, MeasureTheory.eventually_div_right_iff, MeasureTheory.lpNorm_eq_zero, MeasureTheory.measure_preimage_snd_singleton_eq_tsum, MeasureTheory.measure_union_inv_smul, MeasureTheory.MeasuredSets.edist_def, MeasureTheory.measure_unitBall_eq_integral_div_gamma, MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun, ProbabilityTheory.Kernel.parallelComp_apply_univ, HolderOnWith.hausdorffMeasure_image_le, MeasureTheory.mul_meas_ge_le_pow_eLpNorm, dimH_def, MeasureTheory.Integrable.condExpKernel_ae, ae_ae_comm, MeasureTheory.setLIntegral_le_meas, measure_inv, Real.volume_pi_closedBall, MeasureTheory.lintegral_indicator_const₀, MeasureTheory.eLpNorm'_const, exists_isOpen_measure_lt_top, IsCompact.exists_isOpen_lt_add, tendsto_measure_thickening_of_isClosed, restrict_eq_self, MeasureTheory.uIoc_ae_eq_interval, innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint, ae_not_liouvilleWith, ProbabilityTheory.Kernel.densityProcess_def, MeasurableEquiv.map_ae, LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi, MeasureTheory.Ico_ae_eq_Icc, rnDeriv_pos', MeasureTheory.measure_iUnion_toMeasurable, MeasureTheory.ProbabilityMeasure.prod_apply, PreErgodic.aeconst_set, rnDeriv_le_one_of_le, MeasureTheory.Lp.pow_mul_meas_ge_le_enorm, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, LipschitzOnWith.ae_differentiableWithinAt, MeasureTheory.condLExp_add_le, MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_mul, rnDeriv_eq_zero, MeasureTheory.ae_restrict_uIoc_eq, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div_of_integrable, ProbabilityTheory.setBernoulli_apply, MeasureTheory.forall_measure_preimage_add_right_iff, PMF.toMeasure_apply_eq_toOuterMeasure, ProbabilityTheory.HasCondSubgaussianMGF.mgf_le, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div, EMetric.measure_closedBall_pos, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real, MeasureTheory.exp_llr, MeasureTheory.measure_union_add_inter', ProbabilityTheory.Kernel.const_comp, ProbabilityTheory.bayesRisk_const', ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot, MeasureTheory.ae_toFiniteAux, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, MeasureTheory.indicatorConstLp_coeFn, ProbabilityTheory.Kernel.compProd_apply_prod, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrable, measure_Iio_pos, ProbabilityTheory.Kernel.iIndepSets.meas_iInter, ProbabilityTheory.Kernel.rnDeriv_withDensity, lt_iff, sub_apply_eq_zero_of_restrict_le_restrict, IsFoelner.tendsto_nhds_mean, MeasureTheory.Lp.simpleFunc.coeFn_nonneg, ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero, MeasureTheory.exists_measure_iInter_lt, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd, MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup, MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk, Module.Basis.addHaar_self, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot, MeasureTheory.IntegrableAtFilter.inf_ae_iff, IsClosed.ae_eq_univ_iff_eq, le_restrict_apply, volume_regionBetween_eq_lintegral, ProbabilityTheory.ae_eq_posterior_of_compProd_eq, MeasureTheory.AEDisjoint.measure_diff_left, MeasureTheory.measure_mul_setLAverage, MeasureTheory.prob_compl_eq_zero_iff₀, IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero', Real.volume_preimage_mul_right, ProbabilityTheory.Kernel.setLIntegral_rnDerivAux, MeasureTheory.ae_eq_restrict_iUnion_iff, isAddFoelner_iff, ProbabilityTheory.integrable_comp_iff, neg_apply, MeasureTheory.measure_closedBall_lt_top, InnerProductSpace.volume_ball_of_dim_even, PMF.toMeasure_mono, ae_sum_iff', addHaar_singleton, MeasureTheory.Integrable.ae_of_comp, EuclideanSpace.volume_closedBall, ENNReal.essSup_eq_zero_iff, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le, Filter.HasBasis.mem_measureSupport, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, ENNReal.ae_le_essSup, MeasureTheory.condExpL2_comp_continuousLinearMap, MeasureTheory.Lp.coeFn_star, ProbabilityTheory.Kernel.comap_apply', MeasureTheory.exists_isCompact_closure_measure_compl_lt, MeasureTheory.map_div_right_ae, MeasureTheory.Submartingale.ae_le_condExp, MeasureTheory.ae_restrict_union_eq, MeasureTheory.MemLp.meas_ge_lt_top_enorm, count_injective_image, infinitePi_pi_univ, MeasureTheory.toReal_rnDeriv_tilted_right, setLIntegral_condKernel_eq_measure_prod, ProbabilityTheory.Kernel.setLIntegral_rnDeriv_le, VitaliFamily.exists_measurable_supersets_limRatio, MeasureTheory.ae_map_iff_ae_trim, ae_eval_ne, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae', MeasureTheory.trim_comap_apply, MeasureTheory.llr_smul_left, MonotoneOn.ae_differentiableWithinAt, coe_zero, MeasureTheory.volume_sum_rpow_lt_one, MeasureTheory.condExpL2_const_inner, PMF.toMeasure_uniformOfFinset_apply, MeasureTheory.IsFundamentalDomain.measure_eq_tsum, ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero, MeasureTheory.ae_measure_preimage_add_right_lt_top, MeasureTheory.Submartingale.condExp_sub_nonneg, ProbabilityTheory.tilted_mul_apply_cgf', map_snd_prod, coeFn_fourierLp, MeasureTheory.ae_iff_measure_eq, MeasureTheory.self_mem_ae_restrict, PMF.toMeasure_apply_eq_zero_iff, LipschitzWith.ae_differentiableAt_real, MeasureTheory.measureReal_restrict_apply₀', infinitePi_pi_of_countable, MeasureTheory.IsFiniteMeasure.measure_univ_lt_top, ProbabilityTheory.Kernel.swap_apply', ProbabilityTheory.Kernel.tendsto_density_fst_atTop_ae_of_monotone, MeasureTheory.measure_preimage_add, IsCondKernel.apply_of_ne_zero, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, MeasureTheory.lintegral_one, MeasureTheory.measure_preimage_fst_singleton_eq_sum, MeasureTheory.pdf.ofReal_toReal_ae_eq, ProbabilityTheory.Kernel.indepSets_singleton_iff, MeasureTheory.SimpleFunc.finMeasSupp_iff_support, mem_map_indicator_ae_iff_of_zero_notMem, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite, MeasureTheory.Subgroup.index_mul_measure, MeasureTheory.condExp_mul_of_stronglyMeasurable_left, MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc, LinearMap.exists_map_addHaar_eq_smul_addHaar', ProbabilityTheory.ofReal_cdf, MeasureTheory.iInf_mul_le_setLIntegral, Orientation.measure_orthonormalBasis, MeasureTheory.measure_sigmaFiniteSetGE_ge, MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le, toSphere_apply_univ', rnDeriv_smul_right_of_ne_top, IsOpen.measure_eq_zero_iff, IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero, measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop, MeasureTheory.condExp_bot_ae_eq, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀, MeasureTheory.MeasurePreserving.measure_preimage, MeasureTheory.AEEqFun.inv_toGerm, MeasureTheory.Content.measure_apply, ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure, addHaar_closedBall_eq_addHaar_ball, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on, ProbabilityTheory.Kernel.comp_null, MeasureTheory.tilted_apply', MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply, ContinuousLinearMap.coeFn_holder, haarMeasure_eq_iff, MeasureTheory.Integrable.prod_right_ae, MeasureTheory.eLpNorm_indicator_const, MeasureTheory.withDensity_apply, ext_prod_iff, MeasureTheory.ae_lt_top, hausdorffMeasure_of_lt_dimH, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant', ProbabilityTheory.Kernel.fst_compProd_apply, MeasureTheory.ae_comp_linearMap_mem_iff, ae_eq_of_integral_contDiff_smul_eq, BoundedContinuousFunction.lintegral_le_edist_mul, InnerRegularWRT.measurableSet_of_isOpen, ProbabilityTheory.deterministic_comp_posterior, PMF.toMeasure_apply_fintype, addHaar_closedBall', ae_eq_of_integral_smooth_smul_eq, unitInterval.volume_Iio, Real.volume_interval, ZSpan.fundamentalDomain_ae_parallelepiped, ProbabilityTheory.iIndepSets_singleton_iff, ProbabilityTheory.setLIntegral_toKernel_Iic, MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt, MeasureTheory.ae_iff_prob_eq_one, MeasureTheory.Lp.mul_meas_ge_le_pow_enorm, rnDeriv_le_one_iff_le, MeasureTheory.measure_union₀, IsOpen.measure_pos_iff, ae_smul_measure_eq, piContent_eq_infinitePiNat, MeasureTheory.one_le_div_ae, MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero, MeasureTheory.AEEqFun.coeFn_pair, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable, MeasureTheory.SignedMeasure.rnDeriv_add, MeasureTheory.AEEqFun.add_toGerm, ProbabilityTheory.Kernel.prod_apply_prod, ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul, MeasureTheory.neg_llr, iSup_restrict_spanningSets_of_measurableSet, MeasureTheory.AEEqFun.coeFn_one, MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton, MeasureTheory.diracProba_toMeasure_apply_of_mem, MeasureTheory.pdf.ae_lt_top, ContinuousLinearMap.coeFn_compLp', MeasureTheory.forall_measure_preimage_mul_right_iff, MeasureTheory.measure_biUnion₀, PMF.toMeasure_map_apply, PMF.toMeasure_apply_eq_tsum, bind_const, Real.volume_emetric_ball, OuterRegular.measure_closure_eq_of_isCompact, MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem, ProbabilityTheory.Kernel.singularPart_of_subset_mutuallySingularSetSlice, rnDeriv_add_right_of_mutuallySingular, MeasureTheory.AddContent.measureCaratheodory_eq, MeasureTheory.Iio_ae_eq_Iic, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, MeasureTheory.SignedMeasure.rnDeriv_sub, addHaar_smul, PMF.toMeasure_apply_finset, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure, ProbabilityTheory.posterior_comp, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero, instOuterMeasureClass, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null, InnerRegularWRT.exists_subset_lt_add, MeasureTheory.measure_mul_closure_one, addHaar_image_homothety, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, toPMF_apply, measure_isHaarMeasure_eq_smul_of_isOpen, unitInterval.volume_Ioi, MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint
ofMeasurable 📖	CompOp	1 math math: ofMeasurable_apply
real 📖	CompOp	290 math, 1 bridge math: MeasureTheory.tendstoInMeasure_iff_measureReal_norm, MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, InformationTheory.integral_llr_add_mul_log_nonneg, BoxIntegral.Prepartition.measure_iUnion_toReal, MeasureTheory.norm_indicatorConstLp_le, ProbabilityTheory.condDistrib_ae_eq_condExp, Real.volume_real_Ioc, ProbabilityTheory.measure_ge_le_exp_cgf, ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF, MeasureTheory.MeasuredSets.real_sub_real_le_dist, ZSpan.volume_real_fundamentalDomain, MeasureTheory.MeasurePreserving.measureReal_preimage, MeasureTheory.sum_measureReal_singleton, MeasureTheory.weightedSMul_apply, MeasureTheory.probReal_compl_eq_one_sub₀, MeasureTheory.measureReal_symmDiff_le, ProbabilityTheory.unitInterval.cdf_eq_real, InformationTheory.mul_log_le_klDiv, MeasureTheory.integral_unique, MeasureTheory.norm_indicatorConstLp, MeasureTheory.measureReal_le_measureReal_union_left, ProbabilityTheory.integrable_toReal_condExpKernel, ProbabilityTheory.setIntegral_condCDF, ProbabilityTheory.mgf_zero_fun, toSphere_real_apply_univ, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, ProbabilityTheory.IsCondKernelCDF.integral, ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const, MeasureTheory.measureReal_mono, Real.volume_real_Ioo, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge', MeasureTheory.SimpleFunc.integral_eq_sum_filter, ProbabilityTheory.integral_stieltjesOfMeasurableRat, MeasureTheory.measureReal_symmDiff_eq, MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae', norm_sub_le_mul_volume_of_norm_lineDeriv_le, MeasureTheory.ofReal_measureReal, MeasureTheory.measureReal_empty, tendsto_card_div_pow_atTop_volume, ProbabilityTheory.centralMoment_one', integral_toReal_rnDeriv', ContDiffBump.measure_closedBall_div_le_integral, MeasureTheory.probReal_add_probReal_compl, BoundedContinuousFunction.integral_const_sub, MeasureTheory.measure_smul_average, ProbabilityTheory.cgf_zero_fun, Real.volume_real_Ioo_of_le, ProbabilityTheory.Kernel.fst_real_apply, ProbabilityTheory.cdf_eq_real, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff', ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem, ZLattice.covolume.tendsto_card_div_pow, MeasureTheory.setIntegral_condExpL2_indicator, InformationTheory.toReal_klDiv, ContDiffBump.normed_le_div_measure_closedBall_rOut, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, MeasureTheory.integral_singleton', MeasureTheory.measureReal_union_null_iff, MeasureTheory.tendstoInMeasure_iff_measureReal_dist, ZSpan.measureReal_fundamentalDomain, MeasureTheory.measureReal_nonneg, MeasureTheory.setIntegral_condExpInd, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, norm_sub_le_mul_volume_of_norm_deriv_le_of_le, ProbabilityTheory.condExpKernel_ae_eq_condExp', MeasureTheory.measureReal_zero, MeasureTheory.integral_indicatorConstLp, MeasureTheory.measureReal_union_le, ProbabilityTheory.IsCondKernelCDF.setIntegral, MeasureTheory.norm_integral_sub_setIntegral_le, Real.volume_real_Ioc_of_le, MeasureTheory.measureReal_union₀', integral_toReal_rnDeriv, InformationTheory.integral_llr_add_sub_measure_univ_nonneg, MeasureTheory.ProbabilityMeasure.toNNReal_measureReal_eq_coeFn, MeasureTheory.SimpleFunc.integral_eq_sum, MeasureTheory.setIntegral_condExpIndSMul, MeasureTheory.measureReal_biUnion_finset, Real.volume_real_closedBall, MeasureTheory.Lp.norm_const_le, MeasureTheory.measureReal_restrict_apply', MeasureTheory.measureReal_add_apply, InformationTheory.integral_klFun_rnDeriv, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, MeasureTheory.integral_indicator_one, InformationTheory.klDiv_of_ac_of_integrable, ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun, InformationTheory.klDiv_def, MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp, MeasureTheory.measureReal_inter_add_diff₀, MeasureTheory.integral_fintype, MeasureTheory.Lp.norm_const', MeasureTheory.norm_condExpIndL1_le, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul, MeasureTheory.measureReal_add_measureReal_compl₀, integrable_measure_prodMk_left, MeasureTheory.norm_condExpInd_apply_le, MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply, ProbabilityTheory.condExp_set_generateFrom_singleton, addHaar_real_closedBall', setIntegral_toReal_rnDeriv', ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, MeasureTheory.norm_weightedSMul_le, MeasureTheory.measureReal_diff, MeasureTheory.measureReal_iUnion_fintype, MeasureTheory.mul_le_integral_rnDeriv_of_ac, ProbabilityTheory.Kernel.IsFiniteKernel.integrable, BoxIntegral.norm_integral_le_of_le_const, MeasureTheory.setAverage_eq, toSignedMeasure_apply, ZLattice.covolume.tendsto_card_le_div', MeasureTheory.norm_setIntegral_le_of_norm_le_const, MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one, InformationTheory.mul_log_le_toReal_klDiv, ProbabilityTheory.Kernel.setIntegral_densityProcess, ZLattice.covolume_eq_measure_fundamentalDomain, MeasureTheory.Lp.norm_constL_le, ContDiffBump.measure_closedBall_le_integral, ProbabilityTheory.Kernel.integral_densityProcess, MeasureTheory.Integrable.integral_eq_integral_meas_le, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, MeasureTheory.measureReal_union_add_inter₀, MeasureTheory.Integrable.integral_eq_integral_meas_lt, MeasureTheory.norm_integral_le_of_norm_le_const, MeasureTheory.integral_fun_norm_addHaar, MeasureTheory.setIntegral_ge_of_const_le, MeasureTheory.Lp.norm_const, Real.volume_real_Ico_of_le, ProbabilityTheory.hasFiniteIntegral_prodMk_left, MeasureTheory.measureReal_eq_measureReal_iff, ZLattice.covolume_eq_det_mul_measureReal, ProbabilityTheory.condExpKernel_ae_eq_condExp, MeasureTheory.measureReal_ennreal_smul_apply, addHaar_real_closedBall_center, ProbabilityTheory.Kernel.integral_density, MeasureTheory.MeasuredSets.lipschitzWith_measureReal, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, ProbabilityTheory.setIntegral_preCDF_fst, MeasureTheory.measureReal_restrict_apply₀, MeasureTheory.count_real_singleton', MeasureTheory.integral_simpleFunc_larger_space, MeasureTheory.measureReal_abs_gt_le_integral_charFun, intervalIntegral.integral_const_of_cdf, ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp, MeasureTheory.tendstoInMeasure_iff_measureReal_enorm, intervalIntegral.integral_const', ProbabilityTheory.cgf_zero', Real.volume_real_interval, ZLattice.covolume.tendsto_card_div_pow', ProbabilityTheory.cgf_const', Real.volume_real_Icc, MeasureTheory.setIntegral_indicatorConstLp, MeasureTheory.sum_measureReal_preimage_singleton, toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, MeasureTheory.integral_condExp_indicator, setIntegral_toReal_rnDeriv_eq_withDensity', ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF, MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae, MeasureTheory.average_add_measure, MeasureTheory.measureReal_union_add_inter₀', MeasureTheory.FiniteMeasure.measureReal_eq_coe_coeFn, ContDiffBump.integral_le_measure_closedBall, ProbabilityTheory.mgf_const', ZLattice.covolume.tendsto_card_le_div, MeasureTheory.measureReal_union₀, MeasureTheory.measureReal_univ_pos, MeasureTheory.SimpleFunc.integral_eq_sum_of_subset, MeasureTheory.setIntegral_gt_gt, ProbabilityTheory.Kernel.IsMarkovKernel.integrable, ProbabilityTheory.integral_condCDF, MeasureTheory.lpNorm_one, MeasureTheory.integral_const, addHaar_real_ball_center, real_def, MeasureTheory.measureReal_iUnion_fintype_le, MeasureTheory.mul_meas_ge_le_integral_of_nonneg, MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one, MeasureTheory.measureReal_compl₀, MeasureTheory.MeasuredSets.dist_def, MeasureTheory.probReal_univ, MeasureTheory.setIntegral_ge_of_const_le_real, ProbabilityTheory.integrable_kernel_prodMk_left, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le, BoundedContinuousFunction.integral_add_const, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, Real.volume_real_ball, MeasureTheory.setIntegral_one_eq_measureReal, MeasureTheory.measureReal_congr, toBoxAdditive_apply, Real.volume_real_Icc_of_le, MeasureTheory.integral_fun_fst, MeasureTheory.measureReal_union, MeasureTheory.measureReal_le_one, MeasureTheory.measureReal_le_measureReal_union_right, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, MeasureTheory.map_measureReal_apply, ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun, ProbabilityTheory.mgf_zero', MeasureTheory.integral_countable, MeasureTheory.measureReal_compl, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff, MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply, MeasureTheory.measureReal_diff', MeasureTheory.measureReal_union_add_inter', MeasureTheory.measureReal_union', ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, BoundedContinuousFunction.norm_integral_le_mul_norm, MeasureTheory.norm_condExpInd_le, toSignedMeasure_apply_measurable, MeasureTheory.measureReal_def, norm_sub_le_mul_volume_of_norm_fderiv_le, MeasureTheory.integral_indicator_const, Real.volume_real_Ico, ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le, ProbabilityTheory.measure_le_le_exp_mul_mgf, MeasureTheory.measureReal_prod_prod, toSignedMeasure_sub_apply, ContDiffBump.normed_le_div_measure_closedBall_rIn, ProbabilityTheory.measure_ge_le_exp_mul_mgf, MeasureTheory.ProbabilityMeasure.measureReal_eq_coe_coeFn, ProbabilityTheory.Kernel.setIntegral_density, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le, MeasureTheory.measureReal_univ_eq_one, ZLattice.covolume.tendsto_card_le_div'', MeasureTheory.SimpleFunc.integral_const, MeasureTheory.measureReal_biUnion_finset_le, MeasureTheory.integral_singleton, MeasureTheory.measureReal_zero_apply, setIntegral_toReal_rnDeriv_le, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, ProbabilityTheory.integrable_toReal_condDistrib, addHaar_real_closedBall_eq_addHaar_real_ball, tendsto_card_div_pow_atTop_volume', MeasureTheory.measureReal_restrict_apply_univ, MeasureTheory.SimpleFunc.integral_eq, MeasureTheory.le_measureReal_diff, MeasureTheory.measureReal_biUnion_finset₀, ProbabilityTheory.deriv_cgf_zero, MeasureTheory.norm_indicatorConstLp', MeasureTheory.SimpleFunc.map_integral, MeasureTheory.measure_smul_setAverage, setIntegral_toReal_rnDeriv_eq_withDensity, MeasureTheory.condExp_bot', MeasureTheory.measureReal_add_diff, MeasureTheory.lpNorm_one', MeasureTheory.integral_finset, MeasureTheory.measureReal_biUnion_eq_sum_powerset, MeasureTheory.lpNorm_const, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, MeasureTheory.sum_measureReal_le_measureReal_univ, MeasureTheory.charFun_zero, MeasureTheory.measureReal_eq_zero_iff, MeasureTheory.integral_fun_snd, ZLattice.covolume.tendsto_card_div_pow'', MeasureTheory.norm_charFun_le, MeasureTheory.le_integral_rnDeriv_of_ac, MeasureTheory.average_union, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le', ProbabilityTheory.measure_le_le_exp_cgf, MeasureTheory.isProbabilityMeasure_iff_real, setIntegral_toReal_rnDeriv, MeasureTheory.measureReal_diff_le_iff_le_add, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, MeasureTheory.tendsto_integral_meas_thickening_le, MeasureTheory.measureReal_add_measureReal_compl, MeasureTheory.lpNorm_const', ae_eq_const_or_norm_integral_lt_of_norm_le_const, MeasureTheory.norm_condExpIndL1Fin_le, MeasureTheory.measureReal_union_add_inter, MeasureTheory.measureReal_diff_add_inter, MeasureTheory.measureReal_inter_add_diff, MeasureTheory.measureReal_restrict_apply, MeasureTheory.summable_measure_toReal, MeasureTheory.ext_iff_measureReal_singleton, MeasureTheory.integral_countable', MeasureTheory.count_real_singleton, MeasureTheory.probReal_compl_eq_one_sub, InformationTheory.mul_klFun_le_toReal_klDiv, MeasureTheory.condExp_bot_ae_eq, ProbabilityTheory.integral_preCDF_fst, MeasureTheory.measureReal_nnreal_smul_apply, addHaar_real_closedBall, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge, MeasureTheory.average_eq, MeasureTheory.measureReal_restrict_apply_self, MeasureTheory.setIntegral_const bridge: BoxIntegral.hasIntegralIndicatorConst
toOuterMeasure 📖	CompOp	28 math math: outerMeasure_le_iff, sInf_caratheodory, toOuterMeasure_apply, MeasureTheory.toOuterMeasure_toMeasure, zero_toOuterMeasure, coe_toOuterMeasure, restrict_toOuterMeasure_eq_toOuterMeasure_restrict, smul_toOuterMeasure, trimmed, pi_caratheodory, m_iUnion, sInf_apply, MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure, MeasureTheory.boundedBy_measure, toOuterMeasure_injective, MeasureTheory.toMeasure_toOuterMeasure, map_toOuterMeasure, MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure, toOuterMeasure_le, mkMetric'_toOuterMeasure, pi_def, toOuterMeasure_top, MeasureTheory.measure_eq_inducedOuterMeasure, MeasureTheory.measure_eq_trim, MeasureTheory.le_toOuterMeasure_caratheodory, trim_le, add_toOuterMeasure, mkMetric_toOuterMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toOuterMeasure 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal toOuterMeasure MeasureTheory.Measure instFunLike	—	—
ext 📖	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	—	toOuterMeasure_injective trimmed MeasureTheory.OuterMeasure.trim_congr
ext_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	ext
ext_iff' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	ext
instOuterMeasureClass 📖	mathematical	—	MeasureTheory.OuterMeasureClass MeasureTheory.Measure instFunLike	—	MeasureTheory.measure_empty MeasureTheory.OuterMeasure.instOuterMeasureClass MeasureTheory.OuterMeasure.mono MeasureTheory.OuterMeasure.iUnion_nat
m_iUnion 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe MeasureTheory.OuterMeasure ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal toOuterMeasure Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	—
mono_null 📖	—	Set Set.instHasSubset DFunLike.coe MeasureTheory.Measure ENNReal instFunLike instZeroENNReal	—	—	MeasureTheory.measure_mono_null instOuterMeasureClass
ofMeasurable_apply 📖	mathematical	Set Set.instEmptyCollection MeasurableSet.empty ENNReal instZeroENNReal Set.iUnion MeasurableSet.iUnion instCountableNat tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional MeasurableSet	DFunLike.coe MeasureTheory.Measure instFunLike ofMeasurable	—	MeasurableSet.empty MeasurableSet.iUnion instCountableNat MeasureTheory.inducedOuterMeasure_eq
outerMeasure_le_iff 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.OuterMeasure.instPartialOrder toOuterMeasure ENNReal ENNReal.instPartialOrder DFunLike.coe Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Measure instFunLike	—	trimmed MeasureTheory.OuterMeasure.le_trim_iff
real_def 📖	mathematical	—	real ENNReal.toReal DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	MeasureTheory.measureReal_def
toOuterMeasure_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal toOuterMeasure MeasureTheory.Measure instFunLike	—	—
toOuterMeasure_injective 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.OuterMeasure toOuterMeasure	—	—
trim_le 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.OuterMeasure.instPartialOrder MeasureTheory.OuterMeasure.trim toOuterMeasure	—	—
trimmed 📖	mathematical	—	MeasureTheory.OuterMeasure.trim toOuterMeasure	—	le_antisymm trim_le MeasureTheory.OuterMeasure.le_trim

MeasureTheory.MeasureSpace

Definitions

Name	Category	Theorems
toMeasurableSpace 📖	CompOp	546 math math: AddCircle.measure_univ, ProbabilityTheory.lintegral_exponentialPDF_eq_one, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, Real.isFiniteMeasure_restrict_Ioc, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, ProbabilityTheory.paretoCDFReal_eq_lintegral, Real.integrableOn_rpowIntegrand₀₁_Ioi, MonotoneOn.ae_differentiableWithinAt_of_mem, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, SchwartzMap.integral_sesq_fourier_fourier, GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I, Real.volume_real_Ioc, InnerProductSpace.volume_closedBall_of_dim_even, UnitAddTorus.coe_mFourierBasis, Real.smul_map_volume_mul_right, unitInterval.volume_Ioo, unitInterval.volume_Iic, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, ZSpan.volume_real_fundamentalDomain, MeasureTheory.Measure.integral_comp_mul_right, MeasureTheory.volume_pi, unitInterval.volume_def, UnitAddCircle.lintegral_preimage, Real.fourierIntegralInv_eq', MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, volume_iUnion_setOf_liouvilleWith, HasCompactSupport.integral_Ioi_deriv_eq, MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod, volume_set_coe_def, Complex.integral_comp_pi_polarCoord_symm, integrableOn_exp_mul_Iic, UnitAddCircle.intervalIntegral_preimage, MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume, AbsolutelyContinuousOnInterval.ae_differentiableAt, MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume, MeasureTheory.Measure.instIsLocallyFiniteMeasureProdVolume, Real.fourierIntegral_eq, ProbabilityTheory.gammaCDFReal_eq_lintegral, circleIntegral_def_Icc, integral_exp_mul_Iic, ProbabilityTheory.lintegral_gaussianPDF_eq_one, not_integrableOn_Ioi_cpow, MeasureTheory.integral_fintype_prod_volume_eq_pow, ProbabilityTheory.rnDeriv_gaussianReal, SchwartzMap.integral_bilin_fourierInv_eq, MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace, GaussianFourier.integral_cexp_neg_mul_sq_norm, unitInterval.measurePreserving_coe, MeasureTheory.pdf.integral_mul_eq_integral, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, instIsAddHaarMeasureVolume, intervalIntegral.integrableOn_deriv_of_nonneg, Probability.cauchyMeasure_of_scale_ne_zero, Real.rpow_eq_const_mul_integral, MeasureTheory.pdf.IsUniform.mul_pdf_integrable, interval_average_eq_div, ProbabilityTheory.integral_gaussianReal_eq_integral_smul, not_IntegrableOn_Ioi_inv, lintegral_fderiv_lineMap_eq_edist, Real.volume_closedEBall, ProbabilityTheory.lintegral_gammaPDF_of_nonpos, unitInterval.volume_Ico, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, Real.fourier_real_eq_integral_exp_smul, ProbabilityTheory.cdf_paretoMeasure_eq_integral, LocallyBoundedVariationOn.ae_differentiableWithinAt, integrableOn_exp_Iic, unitInterval.volume_apply, Real.volume_closedBall, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, AddCircle.integral_haarAddCircle, Real.smul_map_diagonal_volume_pi, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, Real.volume_val, integral_exp_neg_mul_rpow, integrableOn_Ioi_rpow_of_lt, Real.volume_pi_ball, Real.aestronglyMeasurable_rpowIntegrand₀₁, NumberField.mixedEmbedding.convexBodyLT_volume, integrableOn_Ioi_norm_cpow_of_lt, Complex.integral_rpow_mul_exp_neg_rpow, OrthonormalBasis.measurePreserving_repr, integral_Ioi_rpow_of_lt, SchwartzMap.integral_fourierInv_smul_eq, Complex.volume_sum_rpow_le, ProbabilityTheory.gammaCDFReal_eq_integral, LocallyBoundedVariationOn.ae_differentiableAt, Real.Icc_mem_vitaliFamily_at_left, nullMeasurableSet_region_between_co, setIntegral_Ioi_zero_rpow, SchwartzMap.integral_bilin_fourierIntegral_eq, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg, integral_rpow_mul_exp_neg_rpow, Real.GammaIntegral_convergent, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos', Real.volume_real_Ioo, nullMeasurableSet_regionBetween, Complex.hasDerivAt_GammaIntegral, SchwartzMap.integral_sesq_fourier_eq, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, BoxIntegral.unitPartition.integralSum_eq_tsum_div, Probability.integral_cauchyPDFReal, LipschitzOnWith.ae_differentiableWithinAt_of_mem_real, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, integrableOn_add_rpow_Ioi_of_lt, Monotone.ae_differentiableAt, AddCircle.intervalIntegral_preimage, MeasureTheory.Measure.instSFiniteProdVolume, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, MeasureTheory.Measure.integral_comp_inv_mul_left, curveIntegralFun_trans_aeeq_right, Complex.integral_comp_polarCoord_symm, SchwartzMap.integral_norm_sq_fourier, UnitAddTorus.mFourierCoeff_toLp, Manifold.pathELength_def, EuclideanSpace.volume_closedBall_fin_three, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, integrableOn_Ioi_cpow_iff, Real.volume_preimage_mul_left, integral_exp_mul_complex_Ioi, setIntegral_Ioi_zero_cpow, Real.volume_pi_Ico, nullMeasurableSet_region_between_cc, volume_setOf_liouville, Real.volume_real_Ioo_of_le, AddCircle.instIsAddHaarMeasureRealVolume, Real.map_matrix_volume_pi_eq_smul_volume_pi, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, MeasureTheory.volume_preserving_prodAssoc, BoundedVariationOn.ae_differentiableAt_of_mem_uIcc, Real.volume_Icc_pi, integrableOn_Ioi_norm_cpow_iff, unitInterval.measurePreserving_symm, MeasureTheory.memLp_haarAddCircle_iff, ProbabilityTheory.gaussianReal_of_var_ne_zero, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, AddCircle.ergodic_nsmul_add, Real.smul_map_volume_mul_left, finite_integral_rpow_sub_one_pow_aux, Complex.GammaIntegral_ofReal, Complex.integral_exp_neg_rpow, lintegral_comp_pi_polarCoord_symm, Real.volume_singleton, AddCircle.add_projection_respects_measure, ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv, MeasureTheory.integral_comp_rpow_Ioi_of_pos, Real.volume_pi_Ioc, Real.volume_emetric_closedBall, Real.volume_ball, MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul, intervalIntegral.integrableOn_Ioo_rpow_iff, MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn, Real.volume_Icc_pi_toReal, MeasureTheory.Measure.instIsFiniteMeasureProdVolume, MeasureTheory.Lp.instFourierPair, Real.fourier_real_eq, MeasureTheory.volume_sum_rpow_lt, MeasureTheory.integrable_comp_div_iff, unitInterval.volume_uIcc, ZSpan.volume_fundamentalDomain, unitInterval.volume_Ici, AddCircle.ergodic_add_left, GaussianFourier.integrable_cexp_neg_mul_sum_add, unitInterval.volume_uIoo, LSeries_eq_mul_integral_of_nonneg, Monotone.ae_hasDerivAt, EuclideanSpace.volume_closedBall_fin_two, not_IntegrableOn_Ici_inv, Real.volume_pi_Ioc_toReal, Real.volume_real_Ioc_of_le, AddCircle.ergodic_add_right, BoxIntegral.Box.coe_ae_eq_Icc, mellin_convergent_of_isBigO_scalar, Real.volume_Iio, integral_exp_Iic, UnitAddCircle.measure_univ, integral_mul_cexp_neg_mul_sq, MeasureTheory.integrable_comp, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, AddCircle.instIsUnifLocDoublingMeasureRealVolume, BoxIntegral.Box.Ioo_ae_eq_Icc, Filter.Eventually.volume_pos_of_nhds_real, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, UnitAddTorus.coeFn_mFourierLp, ProbabilityTheory.lintegral_exponentialPDF_of_nonpos, Real.volume_real_closedBall, MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, MeasureTheory.volume_sum_rpow_le, MeasureTheory.VectorMeasure.AbsolutelyContinuous.map, MeasureTheory.integrableOn_Ioi_comp_mul_left_iff, integral_rpow_mul_exp_neg_mul_rpow, MeasureTheory.integral_image_eq_integral_abs_deriv_smul, ProbabilityTheory.integral_gaussianPDFReal_eq_one, integral_comp_polarCoord_symm, Real.volume_Ico, OrthonormalBasis.volume_parallelepiped, AddCircle.volume_closedBall, SchwartzMap.convolution_apply, NumberField.mixedEmbedding.realSpace.volume_eq_zero, Real.pow_mul_norm_iteratedFDeriv_fourier_le, ProbabilityTheory.lintegral_betaPDF_eq_one, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, MeasureTheory.volume_preserving_pi_empty, interval_average_symm, SchwartzMap.integral_bilin_fourier_eq, Chebyshev.integrableOn_theta_div_id_mul_log_sq, unitInterval.volume_Icc, intervalIntegral.integrableOn_Ioo_cpow_iff, volume_regionBetween_eq_lintegral', InnerProductSpace.volume_ball, integrableOn_Ioi_deriv_ofReal_cpow, Real.fourierIntegral_real_eq_integral_exp_smul, MeasureTheory.Lp.norm_fourier_eq, ProbabilityTheory.lintegral_paretoPDF_of_le, MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos, Real.integral_rpowIntegrand₀₁_one_pos, HasCompactSupport.integral_Iic_deriv_eq, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos', not_integrableOn_Ioi_rpow, integral_comp_abs, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, ProbabilityTheory.cdf_gammaMeasure_eq_lintegral, Set.OrdConnected.null_frontier, ProbabilityTheory.gaussianReal_apply, MeasureTheory.lintegral_eq_lintegral_meas_le, MeasureTheory.Pi.isInvInvariant_volume, ProbabilityTheory.lintegral_paretoPDF_eq_one, Real.volume_pi_le_prod_diam, HasCompactSupport.enorm_le_lintegral_Ici_deriv, InnerProductSpace.volume_ball_of_dim_odd, UnitAddTorus.orthonormal_mFourier, BoxIntegral.Box.volume_apply', Real.disjoint_residual_ae, AddCircle.ergodic_nsmul, intervalAverage_congr_codiscreteWithin, Complex.integral_exp_neg_mul_rpow, MeasureTheory.Measure.volume_pi_eq_dirac, Real.fourier_eq, Real.volume_Iic, MeasureTheory.Measure.Subtype.volume_def, MeasureTheory.Measure.integral_comp_mul_left, Real.isFiniteMeasure_restrict_Ioo, Real.volume_Icc, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, MeasureTheory.Integrable.integral_eq_integral_meas_le, MeasurableEmbedding.gaussianReal_comap_apply, TemperedDistribution.fourier_delta_zero, Complex.volume_sum_rpow_lt, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, MeasureTheory.integral_comp_rpow_Ioi, MeasureTheory.Measure.volume_eq_prod, integral_univ_inv_one_add_sq, Complex.lintegral_comp_polarCoord_symm, integrable_rpow_mul_exp_neg_mul_sq, integral_exp_neg_rpow, integrable_mul_exp_neg_mul_sq, Real.volume_pi_Ioo, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, MeasureTheory.Integrable.integral_eq_integral_meas_lt, integral_cexp_quadratic, Manifold.riemannianEDist_def, MeasureTheory.integral_fun_norm_addHaar, UnitAddTorus.hasSum_mFourier_series_L2, unitInterval.instIsProbabilityMeasureElemRealVolume, ProbabilityTheory.exponentialCDFReal_eq_integral, MeasureTheory.integral_comp, ProbabilityTheory.cdf_expMeasure_eq_integral, Real.isFiniteMeasure_restrict_Icc, MeasureTheory.integrable_comp_mul_left_iff, Real.volume_real_Ico_of_le, Real.volume_pi_Ioo_toReal, integrableOn_exp_mul_complex_Iic, SchwartzMap.integral_sesq_fourierIntegral_eq, LSeries_eq_mul_integral, Real.fourierIntegral_eq', ProbabilityTheory.paretoCDFReal_eq_integral, ProbabilityTheory.exp_neg_integrableOn_Ioc, AddCircle.measurePreserving_equivIoc, MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul, MeasureTheory.Pi.isNegInvariant_volume, Real.volume_Ioc, MeasureTheory.Lp.instFourierPairInv, Real.integrable_of_summable_norm_Icc, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter, integrableOn_Ioi_rpow_iff, EuclideanSpace.volume_ball_fin_three, enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, integrableOn_rpow_mul_exp_neg_rpow, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn, integrableOn_exp_mul_Ioi, Complex.volume_closedBall, MeasureTheory.Lp.instFourierInvAdd, Real.isFiniteMeasure_restrict_Ico, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, OrthonormalBasis.measurePreserving_repr_symm, integral_exp_neg_Ioi, Real.volume_eball, UnitAddCircle.measurePreserving_mk, Real.volume_le_diam, integral_comp_neg_Iic, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, Real.volume_real_interval, MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn, Real.volume_real_Icc, integrable_inv_one_add_sq, Real.Gamma_eq_integral, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi, MeasureTheory.Measure.instSigmaFiniteProdVolume, MeasureTheory.lintegral_eq_lintegral_meas_lt, ZLattice.volume_image_eq_volume_div_covolume, Real.map_linearMap_volume_pi_eq_smul_volume_pi, AddCircle.ergodic_zsmul, LipschitzOnWith.ae_differentiableWithinAt_real, Real.le_integral_rpowIntegrand₀₁_one, Probability.lintegral_cauchyPDF_eq_one, integrableOn_exp_neg_Ioi, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, SchwartzMap.integral_fourier_mul_eq, integrable_of_isBigO_exp_neg, EuclideanSpace.volume_ball_fin_two, MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone, NumberField.mixedEmbedding.volume_eq_zero, EuclideanSpace.volume_ball, unitInterval.volume_Ioc, AddCircle.addWellApproximable_ae_empty_or_univ, ProbabilityTheory.lintegral_gaussianPDFReal_eq_one, AddCircle.isFiniteMeasure, integrableOn_Ioi_cpow_of_lt, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, Real.volume_Ici, Real.tendsto_integral_exp_smul_cocompact, intervalIntegral.integrableOn_deriv_right_of_nonneg, GaussianFourier.integral_cexp_neg_mul_sum_add, integral_exp_mul_Ioi, Real.volume_uIoo, fourierIntegral_gaussian, ZLattice.volume_image_eq_volume_div_covolume', Real.volume_pi_Ico_toReal, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, integral_gaussian_sq_complex, Real.volume_pi_le_diam_pow, fourierIntegral_half_period_translate, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg', MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, volume_regionBetween_eq_integral', UnitAddTorus.hasSum_prod_mFourierCoeff, MeasureTheory.integrable_comp_mul_right_iff, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, Real.volume_real_ball, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, Real.volume_real_Icc_of_le, integrableOn_Ioi_exp_neg_mul_sq_iff, MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow, instIsAddHaarMeasureProdRealVolume, Real.locallyFinite_volume, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, MeasureTheory.Lp.inner_fourier_eq, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos, MeasureTheory.MemLp.of_haarAddCircle, MeasureTheory.integral_comp_mul_right_Ioi, AddCircle.lintegral_preimage, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, Manifold.pathELength_eq_lintegral_mfderiv_Icc, ProbabilityTheory.lintegral_betaPDF, Real.circleAverage_eq_intervalAverage, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul, AddCircle.measurePreserving_mk, IsUpperSet.null_frontier, lintegral_comp_polarCoord_symm, integral_comp_neg_Ioi, MeasureTheory.isAddHaarMeasure_volume_pi, instIsProbabilityMeasureUnitAddCircleVolume, ProbabilityTheory.cdf_expMeasure_eq_lintegral, Real.tendsto_Icc_vitaliFamily_left, integral_gaussian, MeasureTheory.volume_preserving_piUnique, SchwartzMap.integral_fourier_smul_eq, Real.map_volume_mul_right, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, GaussianFourier.integral_cexp_neg_sum_mul_add, volume_euclideanSpace_eq_dirac, BoxIntegral.Box.volume_apply, curveIntegralFun_trans_aeeq_left, Complex.integral_rpow_mul_exp_neg_mul_rpow, polarCoord_source_ae_eq_univ, MeasureTheory.pdf.IsUniform.integral_eq, Complex.volume_ball, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, StieltjesFunction.ae_hasDerivAt, norm_sub_le_mul_volume_of_norm_fderiv_le, ProbabilityTheory.gaussianReal_absolutelyContinuous', UnitAddTorus.mFourierBasis_repr, Real.volume_real_Ico, unitInterval.instNoAtomsElemRealVolume, Real.integral_rpow_mul_exp_neg_mul_Ioi, tendsto_integral_exp_inner_smul_cocompact, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, Real.volume_univ, integral_Ioi_cpow_of_lt, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, UnitAddTorus.hasSum_sq_mFourierCoeff, not_integrableOn_Ici_inv, Complex.lintegral_comp_pi_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, volume_regionBetween_eq_integral, exp_neg_integrableOn_Ioi, nullMeasurableSet_region_between_oc, integral_gaussian_complex, integrable_exp_neg_mul_sq_iff, Real.noAtoms_volume, not_integrableOn_Ioi_inv, ae_not_liouville, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, SchwartzMap.integral_inner_fourier_fourier, InnerProductSpace.volume_closedBall, GaussianFourier.integrable_cexp_neg_sum_mul_add, integral_exp_mul_complex_Iic, Probability.integrable_cauchyPDFReal, integrableOn_rpow_mul_exp_neg_mul_sq, SchwartzMap.fourier_convolution_apply, InnerProductSpace.volume_closedBall_of_dim_odd, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, pi_polarCoord_symm_target_ae_eq_univ, AddCircle.integral_liftIoc_eq_intervalIntegral, integral_Ioi_inv_one_add_sq, BoxIntegral.unitPartition.volume_box, Complex.volume_sum_rpow_lt_one, ProbabilityTheory.lintegral_gammaPDF_eq_one, MeasureTheory.integral_comp_mul_left_Ioi, integral_exp_neg_Ioi_zero, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, MeasurableEquiv.gaussianReal_map_symm_apply, SchwartzMap.coe_apply, integral_gaussian_Ioi, integrable_exp_neg_mul_sq, MeasureTheory.volume_preserving_finTwoArrow, AddCircle.closedBall_ae_eq_ball, IntervalIntegrable.ae_hasDerivAt_integral, Real.Icc_mem_vitaliFamily_at_right, Real.volume_uIoc, integrable_cexp_quadratic, Real.fourierInv_eq, unitInterval.volume_uIoc, MeasureTheory.Measure.instIsProbabilityMeasureProdVolume, MeasureTheory.integrableOn_Ioi_comp_mul_right_iff, ProbabilityTheory.cdf_paretoMeasure_eq_lintegral, Real.volume_Ioi, integral_Iic_inv_one_add_sq, interval_average_eq, Real.volume_Ioo, TorusIntegrable.function_integrable, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const, IsAntichain.volume_eq_zero, integrable_mul_cexp_neg_mul_sq, Complex.GammaIntegral_convergent, ProbabilityTheory.gaussianReal_apply_eq_integral, MeasureTheory.integrableOn_Ioi_comp_rpow_iff, NumberField.mixedEmbedding.convexBodySum_volume, MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn, IsLowerSet.null_frontier, MeasureTheory.integrable_fun_norm_addHaar, exists_eq_interval_average, integral_exp_Iic_zero, Real.fourierInv_eq', integrable_cexp_quadratic', OrthonormalBasis.measurePreserving_measurableEquiv, Real.fourierIntegral_real_eq, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, Real.volume_pi_closedBall, SchwartzMap.integral_smul_deriv_right_eq_neg_left, instIsAddHaarMeasureUnitAddCircleVolume, UnitAddTorus.span_mFourierLp_closure_eq_top, ProbabilityTheory.integrable_gaussianPDFReal, ae_not_liouvilleWith, MeasureTheory.Pi.isAddLeftInvariant_volume, Complex.integral_cpow_mul_exp_neg_mul_Ioi, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real, UnitAddCircle.integral_preimage, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg', Real.fourierIntegralInv_eq, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, MeasureTheory.tendsto_integral_meas_thickening_le, volume_regionBetween_eq_lintegral, Real.volume_preimage_mul_right, Real.fourier_eq', InnerProductSpace.volume_ball_of_dim_even, integrable_cexp_neg_mul_sq, integral_pow_abs_sub_uIoc, EuclideanSpace.volume_closedBall, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, AddCircle.integral_preimage, integral_comp_pi_polarCoord_symm, MeasureTheory.volume_preserving_funUnique, LSeries_eq_mul_integral', integrableOn_Ioi_deriv_norm_ofReal_cpow, ProbabilityTheory.exponentialCDFReal_eq_lintegral, ProbabilityTheory.cdf_gammaMeasure_eq_integral, MonotoneOn.ae_differentiableWithinAt, MeasureTheory.volume_sum_rpow_lt_one, continuousAt_gaussian_integral, MeasureTheory.Lp.instFourierAdd, LipschitzWith.ae_differentiableAt_real, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, MeasureTheory.Measure.integral_comp_div, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, Real.integrableOn_rpowIntegrand₀₁_Ici, MeasureTheory.integrableOn_Ioi_comp_rpow_iff', integral_gaussian_complex_Ioi, integrableAtFilter_rpow_atTop_iff, AddCircle.ergodic_zsmul_add, lintegral_Iic_eq_lintegral_Iio_add_Icc, unitInterval.volume_Iio, Real.volume_interval, MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite, MeasureTheory.Pi.isMulLeftInvariant_volume, GaussianFourier.integral_rexp_neg_mul_sq_norm, Real.tendsto_Icc_vitaliFamily_right, integrableOn_rpow_mul_exp_neg_mul_rpow, integrableOn_exp_mul_complex_Ioi, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux, MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn, Real.volume_emetric_ball, MeasureTheory.Measure.integral_comp_inv_mul_right, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, Real.map_volume_mul_left, unitInterval.volume_Ioi
volume 📖	CompOp	806 math math: AddCircle.measure_univ, ProbabilityTheory.lintegral_exponentialPDF_eq_one, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Real.isFiniteMeasure_restrict_Ioc, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, Polynomial.mahlerMeasure_def_of_ne_zero, EulerSine.integral_cos_mul_cos_pow, ProbabilityTheory.paretoCDFReal_eq_lintegral, Real.integrableOn_rpowIntegrand₀₁_Ioi, MonotoneOn.intervalIntegral_slope_le, MonotoneOn.ae_differentiableWithinAt_of_mem, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, integral_cos, SchwartzMap.integral_sesq_fourier_fourier, GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I, Real.volume_real_Ioc, InnerProductSpace.volume_closedBall_of_dim_even, UnitAddTorus.coe_mFourierBasis, Real.smul_map_volume_mul_right, unitInterval.volume_Ioo, unitInterval.volume_Iic, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, ZSpan.volume_real_fundamentalDomain, MeasureTheory.Measure.integral_comp_mul_right, SchwartzMap.inner_fourier_toL2_eq, MeasureTheory.volume_pi, SchwartzMap.toLp_fourierTransformInv_eq, intervalIntegral.inv_smul_integral_comp_div_add, unitInterval.volume_def, UnitAddCircle.lintegral_preimage, Real.fourierIntegralInv_eq', volume_iUnion_setOf_liouvilleWith, HasCompactSupport.integral_Ioi_deriv_eq, integral_sin_mul_cos₂, curveIntegrable_segment, intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm, intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc, Complex.integral_boundary_rect_eq_zero_of_differentiableOn, MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod, volume_set_coe_def, Complex.integral_comp_pi_polarCoord_symm, integrableOn_exp_mul_Iic, UnitAddCircle.intervalIntegral_preimage, intervalIntegral.mul_integral_comp_mul_sub, AbsolutelyContinuousOnInterval.ae_differentiableAt, AbsolutelyContinuousOnInterval.integral_deriv_eq_sub, MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume, MeasureTheory.Measure.instIsLocallyFiniteMeasureProdVolume, Real.fourierIntegral_eq, ProbabilityTheory.gammaCDFReal_eq_lintegral, integral_const_on_unit_interval, circleIntegral_def_Icc, integral_exp_mul_Iic, AddCircle.volume_eq_smul_haarAddCircle, ZLattice.covolume_eq_det_inv, ProbabilityTheory.lintegral_gaussianPDF_eq_one, circleIntegrable_iff, not_integrableOn_Ioi_cpow, MeasureTheory.integral_fintype_prod_volume_eq_pow, intervalIntegral.integral_deriv_of_contDiffOn_uIcc, WeakFEPair.hf_modif_int, intervalIntegrable_bernoulliFun, ProbabilityTheory.rnDeriv_gaussianReal, SchwartzMap.integral_bilin_fourierInv_eq, GaussianFourier.integral_cexp_neg_mul_sq_norm, unitInterval.measurePreserving_coe, Complex.betaIntegral_scaled, MeasureTheory.pdf.integral_mul_eq_integral, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, instIsAddHaarMeasureVolume, intervalIntegral.integral_comp_sub_div, intervalIntegral.integral_comp_mul_left, Continuous.integral_hasStrictDerivAt, intervalIntegral.integrableOn_deriv_of_nonneg, intervalIntegral.integral_comp_mul_sub, Probability.cauchyMeasure_of_scale_ne_zero, Real.rpow_eq_const_mul_integral, interval_average_eq_div, integral_pow, ProbabilityTheory.integral_gaussianReal_eq_integral_smul, not_IntegrableOn_Ioi_inv, intervalIntegral.integral_comp_sub_left, integral_log_sin_zero_pi_div_two, lintegral_fderiv_lineMap_eq_edist, Real.volume_closedEBall, ProbabilityTheory.lintegral_gammaPDF_of_nonpos, unitInterval.volume_Ico, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, integral_exp, integral_inv_of_pos, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, Real.fourier_real_eq_integral_exp_smul, ProbabilityTheory.cdf_paretoMeasure_eq_integral, LocallyBoundedVariationOn.ae_differentiableWithinAt, integral_sin_pow_three, integrableOn_exp_Iic, unitInterval.volume_apply, MeasureTheory.Lp.instFourierInvSMul, Real.volume_closedBall, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, AddCircle.integral_haarAddCircle, Real.smul_map_diagonal_volume_pi, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, Real.volume_val, integral_exp_neg_mul_rpow, IntervalIntegrable.comp_sub_left_iff, Polynomial.Chebyshev.integral_measureT, integrableOn_Ioi_rpow_of_lt, Real.volume_pi_ball, Real.aestronglyMeasurable_rpowIntegrand₀₁, integral_sin_pow_pos, NumberField.mixedEmbedding.convexBodyLT_volume, MeasurableSet.map_coe_volume, integrableOn_Ioi_norm_cpow_of_lt, Complex.integral_rpow_mul_exp_neg_rpow, OrthonormalBasis.measurePreserving_repr, integral_Ioi_rpow_of_lt, SchwartzMap.integral_fourierInv_smul_eq, Complex.volume_sum_rpow_le, ProbabilityTheory.gammaCDFReal_eq_integral, integral_bernoulliFun, Complex.integral_circleTransform, LocallyBoundedVariationOn.ae_differentiableAt, MonotoneOn.intervalIntegrable_deriv, Real.Icc_mem_vitaliFamily_at_left, nullMeasurableSet_region_between_co, setIntegral_Ioi_zero_rpow, SchwartzMap.integral_bilin_fourierIntegral_eq, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg, integral_rpow_mul_exp_neg_rpow, SchwartzMap.toLp_fourierInv_eq, Real.GammaIntegral_convergent, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos', Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, Real.volume_real_Ioo, Set.OrdConnected.nullMeasurableSet, integral_cos_pow, intervalIntegral.integral_comp_sub_right, nullMeasurableSet_regionBetween, Complex.hasDerivAt_GammaIntegral, SchwartzMap.integral_sesq_fourier_eq, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, BoxIntegral.unitPartition.integralSum_eq_tsum_div, Probability.integral_cauchyPDFReal, LipschitzOnWith.ae_differentiableWithinAt_of_mem_real, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, integrableOn_add_rpow_Ioi_of_lt, EulerSine.integral_cos_mul_cos_pow_aux, Monotone.ae_differentiableAt, AddCircle.intervalIntegral_preimage, MeasureTheory.Measure.instSFiniteProdVolume, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, MeasureTheory.Measure.integral_comp_inv_mul_left, curveIntegralFun_trans_aeeq_right, Complex.integral_comp_polarCoord_symm, integral_sin_sq, SchwartzMap.integral_norm_sq_fourier, UnitAddTorus.mFourierCoeff_toLp, Manifold.pathELength_def, EuclideanSpace.volume_closedBall_fin_three, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, integrableOn_Ioi_cpow_iff, Real.volume_preimage_mul_left, integral_exp_mul_complex_Ioi, LinearIsometryEquiv.measurePreserving, setIntegral_Ioi_zero_cpow, Real.volume_pi_Ico, nullMeasurableSet_region_between_cc, intervalIntegral.integral_comp_add_div, volume_setOf_liouville, Real.volume_real_Ioo_of_le, AddCircle.instIsAddHaarMeasureRealVolume, Real.map_matrix_volume_pi_eq_smul_volume_pi, BoundedVariationOn.intervalIntegrable_deriv, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, intervalIntegral.hasSum_intervalIntegral_of_summable_norm, MeasureTheory.volume_preserving_prodAssoc, BoundedVariationOn.ae_differentiableAt_of_mem_uIcc, Real.volume_Icc_pi, MonotoneOn.sum_le_integral, integrableOn_Ioi_norm_cpow_iff, integral_cos_pow_aux, unitInterval.measurePreserving_symm, MeasureTheory.memLp_haarAddCircle_iff, ProbabilityTheory.gaussianReal_of_var_ne_zero, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, AddCircle.ergodic_nsmul_add, Real.volume_eq_stieltjes_id, integral_exp_mul_complex, Real.smul_map_volume_mul_left, finite_integral_rpow_sub_one_pow_aux, Complex.GammaIntegral_ofReal, MonotoneOn.integral_le_sum_Ico, PiLp.volume_preserving_toLp, Chebyshev.integral_one_div_log_sq_isBigO, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton, Orientation.measure_eq_volume, Complex.integral_exp_neg_rpow, lintegral_comp_pi_polarCoord_symm, Real.volume_singleton, AddCircle.add_projection_respects_measure, integral_le_sum_mul_Ico_of_antitone_monotone, ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv, integral_bernoulliFun_eq_zero, MeasureTheory.integral_comp_rpow_Ioi_of_pos, curveIntegral_segment, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Real.volume_pi_Ioc, intervalIntegral.integral_deriv_comp_smul_deriv', ZLattice.covolume_div_covolume_eq_relIndex, Real.volume_emetric_closedBall, AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, SchwartzMap.norm_fourier_toL2_eq, norm_cauchyPowerSeries_le, curveIntegral_def, Real.volume_ball, MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul, intervalIntegral.integrableOn_Ioo_rpow_iff, MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn, Real.volume_Icc_pi_toReal, MeasureTheory.Measure.instIsFiniteMeasureProdVolume, MeasureTheory.Lp.instFourierPair, Real.fourier_real_eq, intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt, MeasureTheory.volume_sum_rpow_lt, MeasureTheory.integrable_comp_div_iff, unitInterval.volume_uIcc, integral_cpow, ZSpan.volume_fundamentalDomain, unitInterval.volume_Ici, AddCircle.ergodic_add_left, GaussianFourier.integrable_cexp_neg_mul_sum_add, MeasureTheory.hausdorffMeasure_pi_real, unitInterval.volume_uIoo, LSeries_eq_mul_integral_of_nonneg, Monotone.ae_hasDerivAt, SchwartzMap.norm_fourierTransformCLM_toL2_eq, EuclideanSpace.volume_closedBall_fin_two, not_IntegrableOn_Ici_inv, Real.volume_pi_Ioc_toReal, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter, Real.volume_real_Ioc_of_le, intervalIntegral.integral_deriv_comp_mul_deriv', AddCircle.ergodic_add_right, AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub, BoxIntegral.Box.coe_ae_eq_Icc, intervalIntegral.smul_integral_comp_mul_sub, Real.volume_Iio, EulerSine.sin_pi_mul_eq, integral_exp_Iic, Chebyshev.primeCounting_eq_theta_div_log_add_integral, UnitAddCircle.measure_univ, integral_mul_cexp_neg_mul_sq, MeasureTheory.integrable_comp, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, AddCircle.instIsUnifLocDoublingMeasureRealVolume, BoxIntegral.Box.Ioo_ae_eq_Icc, Filter.Eventually.volume_pos_of_nhds_real, intervalIntegral.integral_comp_smul_deriv'', UnitAddTorus.coeFn_mFourierLp, intervalIntegral.integral_comp_smul_deriv, ProbabilityTheory.lintegral_exponentialPDF_of_nonpos, Polynomial.intervalIntegrable_mahlerMeasure, Real.volume_real_closedBall, MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, intervalIntegrable_sub_inv_iff, intervalIntegral.integral_comp_add_mul, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, integral_sin_pow_mul_cos_pow_odd, MeasureTheory.volume_sum_rpow_le, MeasureTheory.integrableOn_Ioi_comp_mul_left_iff, integral_rpow_mul_exp_neg_mul_rpow, MeasureTheory.integral_image_eq_integral_abs_deriv_smul, ProbabilityTheory.integral_gaussianPDFReal_eq_one, integral_exp_mul_I_eq_sinc, integral_comp_polarCoord_symm, Real.volume_Ico, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left, OrthonormalBasis.volume_parallelepiped, integral_id, AddCircle.volume_closedBall, SchwartzMap.convolution_apply, NumberField.mixedEmbedding.realSpace.volume_eq_zero, ProbabilityTheory.lintegral_betaPDF_eq_one, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, MeasureTheory.volume_preserving_pi_empty, interval_average_symm, intervalIntegral.integral_congr_codiscreteWithin, SchwartzMap.integral_bilin_fourier_eq, Chebyshev.integrableOn_theta_div_id_mul_log_sq, MonotoneOn.intervalIntegrable_slope, unitInterval.volume_Icc, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, intervalIntegral.integrableOn_Ioo_cpow_iff, volume_regionBetween_eq_lintegral', InnerProductSpace.volume_ball, integrableOn_Ioi_deriv_ofReal_cpow, Real.fourierIntegral_real_eq_integral_exp_smul, integral_exp_mul_I_eq_sin, MeasureTheory.Lp.norm_fourier_eq, AntitoneOn.sum_le_integral_Ico, NumberField.mixedEmbedding.covolume_idealLattice, ProbabilityTheory.lintegral_paretoPDF_of_le, MonotoneOn.intervalIntegral_deriv_mem_uIcc, NumberField.mixedEmbedding.volume_preserving_negAt, MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn, MeasureTheory.Lp.instFourierSMul, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos, integral_sin_mul_cos₁, intervalIntegral.smul_integral_comp_sub_mul, Real.integral_rpowIntegrand₀₁_one_pos, HasCompactSupport.integral_Iic_deriv_eq, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos', not_integrableOn_Ioi_rpow, integral_sin_pow_aux, integral_comp_abs, MeasureTheory.hausdorffMeasure_prod_real, integral_div_sq_add_sq, Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, intervalIntegral.integral_deriv_comp_smul_deriv, ProbabilityTheory.cdf_gammaMeasure_eq_lintegral, Set.OrdConnected.null_frontier, ProbabilityTheory.gaussianReal_apply, MonotoneOn.sum_le_integral_Ico, MeasureTheory.lintegral_eq_lintegral_meas_le, MeasureTheory.Pi.isInvInvariant_volume, ProbabilityTheory.lintegral_paretoPDF_eq_one, intervalIntegral.inv_smul_integral_comp_sub_div, Real.volume_pi_le_prod_diam, NumberField.Units.regOfFamily_of_isMaxRank, intervalIntegral.inv_mul_integral_comp_add_div, PiLp.volume_preserving_ofLp, integral_sin_pow_even_mul_cos_pow_even, sum_mul_Ico_le_integral_of_monotone_antitone, HasCompactSupport.enorm_le_lintegral_Ici_deriv, InnerProductSpace.volume_ball_of_dim_odd, MeasureTheory.integral_charFun_Icc, UnitAddTorus.orthonormal_mFourier, BoxIntegral.Box.volume_apply', intervalIntegral.inv_mul_integral_comp_sub_div, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, Real.disjoint_residual_ae, Real.circleAverage_def, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, intervalIntegral.integral_comp_div, AddCircle.ergodic_nsmul, intervalAverage_congr_codiscreteWithin, Complex.integral_exp_neg_mul_rpow, MeasureTheory.Measure.volume_pi_eq_dirac, Real.fourier_eq, Real.volume_Iic, MeasureTheory.Measure.Subtype.volume_def, integral_inv_of_neg, MeasureTheory.Measure.integral_comp_mul_left, Function.Periodic.intervalIntegral_add_eq_of_pos, Real.isFiniteMeasure_restrict_Ioo, Real.volume_Icc, intervalIntegral.integral_comp_mul_deriv, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, AntitoneOn.integral_le_sum_Ico, Real.circleAverage_eq_integral_add, intervalIntegral.inv_smul_integral_comp_div_sub, MeasureTheory.Integrable.integral_eq_integral_meas_le, MeasurableEmbedding.gaussianReal_comap_apply, TemperedDistribution.fourier_delta_zero, intervalIntegral.mul_integral_comp_add_mul, Complex.volume_sum_rpow_lt, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, MeasureTheory.integral_comp_rpow_Ioi, MeasureTheory.Measure.volume_eq_prod, integral_univ_inv_one_add_sq, Complex.lintegral_comp_polarCoord_symm, integrable_rpow_mul_exp_neg_mul_sq, integral_exp_neg_rpow, integrable_mul_exp_neg_mul_sq, Real.volume_pi_Ioo, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, MeasureTheory.Integrable.integral_eq_integral_meas_lt, integral_cexp_quadratic, integral_inv, Manifold.riemannianEDist_def, MeasureTheory.integral_fun_norm_addHaar, MeasureTheory.Lp.instContinuousFourierInv, UnitAddTorus.hasSum_mFourier_series_L2, unitInterval.instIsProbabilityMeasureElemRealVolume, ProbabilityTheory.exponentialCDFReal_eq_integral, MeasureTheory.integral_comp, ProbabilityTheory.cdf_expMeasure_eq_integral, Real.isFiniteMeasure_restrict_Icc, Complex.volume_preserving_equiv_real_prod, MeasureTheory.integrable_comp_mul_left_iff, Real.volume_real_Ico_of_le, Real.volume_pi_Ioo_toReal, integral_cos_pow_three, integrableOn_exp_mul_complex_Iic, SchwartzMap.integral_sesq_fourierIntegral_eq, LSeries_eq_mul_integral, Real.fourierIntegral_eq', intervalIntegral.integral_comp_smul_deriv', ProbabilityTheory.paretoCDFReal_eq_integral, Real.hasPDF_iff, integral_one_div_of_pos, ProbabilityTheory.exp_neg_integrableOn_Ioc, AddCircle.measurePreserving_equivIoc, intervalIntegral.integral_comp_sub_mul, NumberField.mixedEmbedding.covolume_integerLattice, MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul, MeasureTheory.Pi.isNegInvariant_volume, Real.volume_Ioc, MeasureTheory.Lp.instFourierPairInv, Real.integrable_of_summable_norm_Icc, intervalIntegral.smul_integral_comp_mul_left, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter, integrableOn_Ioi_rpow_iff, EuclideanSpace.volume_ball_fin_three, enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, integral_log_sin_zero_pi, integrableOn_rpow_mul_exp_neg_rpow, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured, integrableOn_exp_mul_Ioi, Complex.volume_closedBall, Real.hasPDF_iff_of_aemeasurable, integral_inv_sq_add_sq, MeasureTheory.Lp.instFourierInvAdd, Real.isFiniteMeasure_restrict_Ico, IntervalIntegrable.comp_mul_left_iff, integral_rpow, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, OrthonormalBasis.measurePreserving_repr_symm, MeasureTheory.measureReal_abs_gt_le_integral_charFun, integral_exp_neg_Ioi, Real.volume_eball, UnitAddCircle.measurePreserving_mk, MeasureTheory.addHaarMeasure_eq_volume_pi, Real.volume_le_diam, integral_comp_neg_Iic, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, Real.volume_real_interval, MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn, integral_log, Real.volume_real_Icc, integral_sqrt_one_sub_sq, integrable_inv_one_add_sq, Real.Gamma_eq_integral, LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi, MeasureTheory.Measure.instSigmaFiniteProdVolume, MeasureTheory.lintegral_eq_lintegral_meas_lt, intervalIntegrable_posLog_norm_meromorphicOn, ZLattice.volume_image_eq_volume_div_covolume, Real.map_linearMap_volume_pi_eq_smul_volume_pi, intervalIntegral.inv_mul_integral_comp_div_sub, intervalIntegral.differentiable_integral_of_continuous, intervalIntegral.smul_integral_comp_mul_add, integral_log_from_zero_of_pos, EulerSine.integral_cos_pow_eq, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, AddCircle.ergodic_zsmul, Complex.betaIntegral_convergent, LipschitzOnWith.ae_differentiableWithinAt_real, integral_sin, fourierCoeff_eq_intervalIntegral, intervalIntegral.integral_comp_add_right, Real.le_integral_rpowIntegrand₀₁_one, LindemannWeierstrass.integral_exp_mul_eval, intervalIntegral.inv_smul_integral_comp_div, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, Probability.lintegral_cauchyPDF_eq_one, intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc, SchwartzMap.inner_fourierTransformCLM_toL2_eq, integrableOn_exp_neg_Ioi, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, SchwartzMap.integral_fourier_mul_eq, Complex.volume_preserving_equiv_pi, Complex.wedgeIntegral_add_wedgeIntegral_eq, intervalIntegrable_log_cos, integral_sin_pow_odd_mul_cos_pow, Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable, EulerSine.tendsto_integral_cos_pow_mul_div, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, integrable_of_isBigO_exp_neg, EuclideanSpace.volume_ball_fin_two, MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone, NumberField.mixedEmbedding.volume_eq_zero, bernoulliFun_eq_integral, EuclideanSpace.volume_ball, unitInterval.volume_Ioc, AddCircle.addWellApproximable_ae_empty_or_univ, ProbabilityTheory.lintegral_gaussianPDFReal_eq_one, intervalIntegral.intervalIntegrable_deriv_of_nonneg, AddCircle.isFiniteMeasure, integrableOn_Ioi_cpow_of_lt, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, curveIntegral_eq_intervalIntegral_deriv, Real.volume_Ici, Real.tendsto_integral_exp_smul_cocompact, intervalIntegral.integrableOn_deriv_right_of_nonneg, GaussianFourier.integral_cexp_neg_mul_sum_add, integral_exp_mul_Ioi, integral_sin_mul_cos_sq, Real.volume_uIoo, fourierIntegral_gaussian, Complex.integrable_pow_mul_norm_one_add_mul_inv, Real.volume_pi_Ico_toReal, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, integral_gaussian_sq_complex, SchwartzMap.toLp_fourierTransform_eq, Real.volume_pi_le_diam_pow, fourierIntegral_half_period_translate, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg', MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, volume_regionBetween_eq_integral', UnitAddTorus.hasSum_prod_mFourierCoeff, MeasureTheory.integrable_comp_mul_right_iff, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, MeasureTheory.hausdorffMeasure_real, ODE.FunSpace.intervalIntegrable_comp_compProj, Real.volume_real_ball, intervalIntegral.integral_deriv_eq_sub', MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, intervalIntegral.mul_integral_comp_mul_add, Real.volume_real_Icc_of_le, integrableOn_Ioi_exp_neg_mul_sq_iff, Complex.GammaSeq_eq_approx_Gamma_integral, MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow, instIsAddHaarMeasureProdRealVolume, Real.locallyFinite_volume, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, MeasureTheory.Lp.inner_fourier_eq, intervalIntegral.integral_deriv_comp_mul_deriv, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos, integral_zpow, MeasureTheory.MemLp.of_haarAddCircle, MeasureTheory.integral_comp_mul_right_Ioi, AddCircle.lintegral_preimage, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add, integral_one_div_one_add_sq, Complex.log_eq_integral, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, integral_one, Manifold.pathELength_eq_lintegral_mfderiv_Icc, ProbabilityTheory.lintegral_betaPDF, MeasureTheory.integral_subtype, IntervalIntegrable.iff_comp_neg, Real.circleAverage_eq_intervalAverage, MeromorphicOn.intervalIntegrable_log, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, integral_sin_pow_succ_le, MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul, AddCircle.measurePreserving_mk, IsUpperSet.null_frontier, circleIntegrable_def, lintegral_comp_polarCoord_symm, integral_comp_neg_Ioi, intervalIntegral.norm_integral_le_of_norm_le_const, Continuous.deriv_integral, MeasureTheory.isAddHaarMeasure_volume_pi, Chebyshev.integral_theta_div_log_sq_isBigO, instIsProbabilityMeasureUnitAddCircleVolume, WeakFEPair.hg_int, intervalIntegral.smul_integral_comp_mul_right, ProbabilityTheory.cdf_expMeasure_eq_lintegral, Real.tendsto_Icc_vitaliFamily_left, intervalIntegral.integral_comp_div_add, integral_gaussian, MeasureTheory.volume_preserving_piUnique, intervalIntegral.mul_integral_comp_sub_mul, integral_one_div, SchwartzMap.integral_fourier_smul_eq, Real.map_volume_mul_right, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, GaussianFourier.integral_cexp_neg_sum_mul_add, volume_euclideanSpace_eq_dirac, integral_sin_sq_mul_cos, BoxIntegral.Box.volume_apply, curveIntegralFun_trans_aeeq_left, WeakFEPair.hf_int, Complex.integral_rpow_mul_exp_neg_mul_rpow, polarCoord_source_ae_eq_univ, not_intervalIntegrable_of_sub_inv_isBigO_punctured, Chebyshev.integral_theta_div_log_sq_isLittleO, EulerSine.integral_cos_pow_pos, MonotoneOn.integral_le_sum, AntitoneOn.sum_le_integral, Complex.volume_ball, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, StieltjesFunction.ae_hasDerivAt, norm_sub_le_mul_volume_of_norm_fderiv_le, ProbabilityTheory.gaussianReal_absolutelyContinuous', UnitAddTorus.mFourierBasis_repr, Real.volume_real_Ico, unitInterval.instNoAtomsElemRealVolume, Real.integral_rpow_mul_exp_neg_mul_Ioi, tendsto_integral_exp_inner_smul_cocompact, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, integral_inv_one_add_sq, Real.volume_univ, integral_Ioi_cpow_of_lt, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, intervalIntegral.mul_integral_comp_mul_right, intervalIntegral.intervalIntegrable_cpow', intervalIntegral.integral_comp_add_left, UnitAddTorus.hasSum_sq_mFourierCoeff, not_integrableOn_Ici_inv, fourierCoeffOn_eq_integral, integral_sin_pow_odd, intervalIntegral.intervalIntegrable_rpow', MeasureTheory.addHaarMeasure_eq_volume, Complex.lintegral_comp_pi_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, volume_regionBetween_eq_integral, ZetaAsymptotics.term_welldef, exp_neg_integrableOn_Ioi, intervalIntegral.integral_comp_mul_right, nullMeasurableSet_region_between_oc, integral_gaussian_complex, intervalIntegral.integral_comp_div_sub, integrable_exp_neg_mul_sq_iff, Real.noAtoms_volume, not_integrableOn_Ioi_inv, intervalIntegral.inv_mul_integral_comp_div, ae_not_liouville, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, intervalIntegrable_log_norm_meromorphicOn, SchwartzMap.integral_inner_fourier_fourier, InnerProductSpace.volume_closedBall, GaussianFourier.integrable_cexp_neg_sum_mul_add, integral_exp_mul_complex_Iic, Probability.integrable_cauchyPDFReal, integrableOn_rpow_mul_exp_neg_mul_sq, SchwartzMap.fourier_convolution_apply, InnerProductSpace.volume_closedBall_of_dim_odd, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, intervalIntegral.integral_comp_mul_deriv', pi_polarCoord_symm_target_ae_eq_univ, AddCircle.integral_liftIoc_eq_intervalIntegral, integral_Ioi_inv_one_add_sq, BoxIntegral.unitPartition.volume_box, Complex.volume_sum_rpow_lt_one, Complex.betaIntegral_convergent_left, ProbabilityTheory.lintegral_gammaPDF_eq_one, MeasureTheory.integral_comp_mul_left_Ioi, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, integral_exp_neg_Ioi_zero, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, MeasurableEquiv.gaussianReal_map_symm_apply, intervalIntegral.integral_comp_mul_add, intervalIntegral.integral_pos, integral_sin_pow, SchwartzMap.coe_apply, integral_mul_cpow_one_add_sq, AntitoneOn.integral_le_sum, integral_gaussian_Ioi, Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn, integrable_exp_neg_mul_sq, MeasureTheory.volume_preserving_finTwoArrow, CircleIntegrable.out, AddCircle.closedBall_ae_eq_ball, Real.Icc_mem_vitaliFamily_at_right, curveIntegral_def', Real.volume_uIoc, integrable_cexp_quadratic, integral_sin_sq_mul_cos_sq, integral_mul_rpow_one_add_sq, Real.fourierInv_eq, unitInterval.volume_uIoc, MeasureTheory.Measure.instIsProbabilityMeasureProdVolume, MeasureTheory.integrableOn_Ioi_comp_mul_right_iff, ProbabilityTheory.cdf_paretoMeasure_eq_lintegral, Chebyshev.intervalIntegrable_one_div_log_sq, MeasureTheory.intervalIntegrable_charFun, Real.volume_Ioi, integral_Iic_inv_one_add_sq, interval_average_eq, Real.volume_Ioo, integral_cos_sq, TorusIntegrable.function_integrable, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const, IsAntichain.volume_eq_zero, integrable_mul_cexp_neg_mul_sq, Complex.GammaIntegral_convergent, intervalIntegral.integral_unitInterval_deriv_eq_sub, ProbabilityTheory.gaussianReal_apply_eq_integral, OrthonormalBasis.addHaar_eq_volume, MeasureTheory.integrableOn_Ioi_comp_rpow_iff, NumberField.mixedEmbedding.convexBodySum_volume, MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn, IsLowerSet.null_frontier, MeasureTheory.integrable_fun_norm_addHaar, volume_image_subtype_coe, exists_eq_interval_average, integral_exp_Iic_zero, Real.fourierInv_eq', MeasureTheory.Lp.instContinuousFourier, integral_log_from_zero, intervalIntegral.integral_comp_neg, integrable_cexp_quadratic', OrthonormalBasis.measurePreserving_measurableEquiv, Real.fourierIntegral_real_eq, integral_cos_sq_sub_sin_sq, Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, Real.volume_pi_closedBall, SchwartzMap.integral_smul_deriv_right_eq_neg_left, instIsAddHaarMeasureUnitAddCircleVolume, Complex.log_inv_eq_integral, UnitAddTorus.span_mFourierLp_closure_eq_top, AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul, intervalIntegral.inv_mul_integral_comp_div_add, ProbabilityTheory.integrable_gaussianPDFReal, ae_not_liouvilleWith, MeasureTheory.Pi.isAddLeftInvariant_volume, Complex.integral_cpow_mul_exp_neg_mul_Ioi, integral_cos_mul_complex, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_right, intervalIntegral.integral_comp_mul_deriv'', LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real, Real.volume_preserving_transvectionStruct, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, UnitAddCircle.integral_preimage, integral_one_div_of_neg, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg', Real.fourierIntegralInv_eq, Complex.approx_Gamma_integral_tendsto_Gamma_integral, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, SchwartzMap.toLp_fourier_eq, MeasureTheory.tendsto_integral_meas_thickening_le, Function.Periodic.intervalIntegral_add_eq, volume_regionBetween_eq_lintegral, Real.volume_preimage_mul_right, Real.fourier_eq', integral_sin_pow_antitone, InnerProductSpace.volume_ball_of_dim_even, integrable_cexp_neg_mul_sq, intervalIntegrable_log_sin, integral_pow_abs_sub_uIoc, EuclideanSpace.volume_closedBall, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, intervalIntegrable_inv_iff, AddCircle.integral_preimage, integral_comp_pi_polarCoord_symm, MeasureTheory.volume_preserving_funUnique, LSeries_eq_mul_integral', integrableOn_Ioi_deriv_norm_ofReal_cpow, ProbabilityTheory.exponentialCDFReal_eq_lintegral, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv, ProbabilityTheory.cdf_gammaMeasure_eq_integral, MonotoneOn.ae_differentiableWithinAt, MeasureTheory.volume_sum_rpow_lt_one, intervalIntegral.intervalIntegrable_log', continuousAt_gaussian_integral, intervalIntegral.integral_deriv_of_contDiffOn_Icc, ZLattice.covolume_div_covolume_eq_relIndex', MeasureTheory.Lp.instFourierAdd, LipschitzWith.ae_differentiableAt_real, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, EulerSine.integral_cos_mul_cos_pow_even, integral_sin_pow_even, MeasureTheory.Measure.integral_comp_div, intervalIntegral.integral_const, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, Real.integrableOn_rpowIntegrand₀₁_Ici, MeasureTheory.integrableOn_Ioi_comp_rpow_iff', integral_gaussian_complex_Ioi, ODE.picard_apply, integrableAtFilter_rpow_atTop_iff, AddCircle.ergodic_zsmul_add, lintegral_Iic_eq_lintegral_Iio_add_Icc, unitInterval.volume_Iio, Real.volume_interval, MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite, MeasureTheory.Pi.isMulLeftInvariant_volume, intervalIntegral.inv_smul_integral_comp_add_div, ZLattice.covolume_eq_det, GaussianFourier.integral_rexp_neg_mul_sq_norm, Real.tendsto_Icc_vitaliFamily_right, integrableOn_rpow_mul_exp_neg_mul_rpow, intervalIntegral.differentiableOn_integral_of_continuous, integrableOn_exp_mul_complex_Ioi, ProbabilityTheory.gaussianReal_absolutelyContinuous, not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux, MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn, Real.volume_emetric_ball, intervalIntegral.smul_integral_comp_add_mul, MeasureTheory.Measure.integral_comp_inv_mul_right, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, intervalIntegral.mul_integral_comp_mul_left, Real.map_volume_mul_left, unitInterval.volume_Ioi

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass AEMeasurable.congr Filter.EventuallyEq.symm
aemeasurable_const 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_const
aemeasurable_id 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_id
aemeasurable_id' 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_id
aemeasurable_pi_iff 📖	mathematical	—	AEMeasurable MeasurableSpace.pi	—	AEMeasurable.eval MeasureTheory.Measure.instOuterMeasureClass measurable_pi_lambda Filter.Eventually.mono eventually_countable_forall MeasureTheory.instCountableInterFilter
aemeasurable_pi_lambda 📖	mathematical	AEMeasurable	MeasurableSpace.pi	—	aemeasurable_pi_iff

---

← Back to Index