Documentation Verification Report

StronglyMeasurable

📁 Source: Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean

Statistics

MetricCount
DefinitionsStronglyMeasurable
1
TheoremslimUnder, measurableSet_exists_tendsto
2
Total3

MeasureTheory

Definitions

NameCategoryTheorems
StronglyMeasurable 📖MathDef
164 mathmath: stronglyMeasurable_const, StronglyMeasurable.integral_kernel_prod_right'', stronglyMeasurable_of_restrict_of_restrict_compl, StronglyMeasurable.neg, StronglyMeasurable.div₀, ProbabilityTheory.stronglyMeasurable_cauchyPDFReal, StronglyMeasurable.vadd_const, Finset.stronglyMeasurable_prod, StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on, finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite, StronglyMeasurable.mul_iff_left, Multiset.stronglyMeasurable_fun_prod, StronglyMeasurable.add_iff_right, StronglyMeasurable.integral_prod_left, Finset.stronglyMeasurable_fun_sum, stronglyMeasurable_derivWithin_Ioi, stronglyMeasurable_of_stronglyMeasurable_union_cover, Continuous.stronglyMeasurable_of_hasCompactSupport, ProbabilityTheory.stronglyMeasurable_geometricPMFReal, StronglyMeasurable.prod_swap, stronglyMeasurable_of_tendsto, IsUnit.stronglyMeasurable_const_smul_iff, StronglyMeasurable.sub, MeasurableEmbedding.exists_stronglyMeasurable_extend, Continuous.stronglyMeasurable_of_hasCompactMulSupport, StronglyMeasurable.const_nsmul, Lp.stronglyMeasurable, StronglyMeasurable.integral_kernel_prod_right, ProbabilityTheory.stronglyMeasurable_integral_condDistrib, Lp.simpleFunc.stronglyMeasurable, List.stronglyMeasurable_fun_prod, Measurable.stronglyMeasurable, StronglyMeasurable.sup, StronglyMeasurable.snd, StronglyMeasurable.inner, StronglyMeasurable.of_uncurry_right, StronglyMeasurable.edist, stronglyMeasurable_lineDeriv, stronglyMeasurable_id, StronglyMeasurable.mul_iff_right, StronglyMeasurable.smul, ProbabilityTheory.stronglyMeasurable_condExpKernel, StronglyMeasurable.const_mul, ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction, StronglyMeasurable.inv, StronglyMeasurable.fst, ProbabilityTheory.stronglyMeasurable_poissonPMFReal, StronglyMeasurable.integral_kernel_prod_right', StronglyMeasurable.integral_condExpKernel, stronglyMeasurable_one, StronglyMeasurable.vadd, Finset.stronglyMeasurable_sum, StronglyAdapted.stronglyMeasurable_stoppedProcess, StronglyMeasurable.of_subsingleton_cod, StronglyMeasurable.exists_eq_measurable_comp, StronglyMeasurable.real_toNNReal, stronglyMeasurable_iff_measurable_separable, Multiset.stronglyMeasurable_sum, Submartingale.stronglyMeasurable, StronglyMeasurable.smul_const, stronglyMeasurable_const_smul_iff, StronglyMeasurable.of_discrete, stronglyMeasurable_lineDeriv_uncurry, condExp_def, StronglyMeasurable.inf, StronglyMeasurable.div, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist, StronglyAdapted.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat, AEStronglyMeasurable.stronglyMeasurable_mk, Continuous.stronglyMeasurable, StronglyMeasurable.integral_condExpKernel', StronglyMeasurable.integral_condDistrib, StronglyMeasurable.comp_measurable, Finset.stronglyMeasurable_fun_prod, Real.stronglyMeasurable_sinc, StronglyMeasurable.integral_prod_right', StronglyMeasurable.mul, MeasurableEmbedding.stronglyMeasurable_extend, stronglyMeasurable_llr, Supermartingale.stronglyMeasurable, ProgMeasurable.stronglyMeasurable_stoppedProcess, Filtration.stronglyMeasurable_limit_process', stronglyMeasurable_deriv, StronglyMeasurable.comp_snd, Continuous.comp_stronglyMeasurable, StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete, StronglyMeasurable.indicator, exists_stronglyMeasurable_limit_of_tendsto_ae, ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess, StronglyMeasurable.add_iff_left, Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact, stronglyMeasurable_condExp, StronglyMeasurable.pow, StronglyMeasurable.mono, StronglyMeasurable.div', L1.stronglyMeasurable_coeFn, StronglyMeasurable.mul_const, ProbabilityTheory.condVar_of_sigmaFinite, StronglyAdapted.stronglyMeasurable_le, StronglyMeasurable.integral_kernel_prod_left'', FinStronglyMeasurable.stronglyMeasurable, StronglyMeasurable.prodMk, stronglyMeasurable_charFun, InformationTheory.stronglyMeasurable_klFun, stronglyMeasurable_derivWithin_Ici, StronglyMeasurable.const_smul, StronglyMeasurable.apply_continuousLinearMap, ProbabilityTheory.stronglyMeasurable_cauchyPDF, StronglyMeasurable.integral_prod_left', StronglyMeasurable.nnnorm, ProbabilityTheory.stronglyMeasurable_gaussianPDFReal, SimpleFunc.stronglyMeasurable, Embedding.comp_stronglyMeasurable_iff, StronglyMeasurable.norm, condExp_of_sigmaFinite, StronglyMeasurable.Finset.stronglyMeasurable_prod_apply, StronglyMeasurable.limUnder, StronglyMeasurable.sinc, ProbabilityTheory.stronglyMeasurable_condCDF, Continuous.stronglyMeasurable_of_support_subset_isCompact, IndexedPartition.stronglyMeasurable_piecewise, stronglyMeasurable_bot_iff, List.stronglyMeasurable_prod, ProbabilityTheory.stronglyMeasurable_gammaPDFReal, stronglyMeasurable_zero, stronglyMeasurable_iff_measurable, List.stronglyMeasurable_fun_sum, StronglyMeasurable.ite, StronglyMeasurable.const_vadd', stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable, StronglyMeasurable.of_subsingleton_dom, HasCompactSupport.stronglyMeasurable_of_prod, StronglyMeasurable.integral_prod_right, stronglyMeasurable_deriv_with_param, AEEqFun.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_betaPDFReal, StronglyMeasurable.piecewise, Multiset.stronglyMeasurable_fun_sum, List.stronglyMeasurable_sum, StronglyMeasurable.add_const, stronglyMeasurable_const', StronglyMeasurable.integral_kernel_prod_left', Multiset.stronglyMeasurable_prod, AEStronglyMeasurable.exists_stronglyMeasurable_range_subset, StronglyMeasurable.const_add, stronglyMeasurable_const_smul_iff₀, StronglyMeasurable.comp_fst, Martingale.stronglyMeasurable, StronglyMeasurable.dist, ProbabilityTheory.stronglyMeasurable_paretoPDFReal, StronglyMeasurable.integral_kernel, StronglyMeasurable.integral_kernel_prod_left, StronglyMeasurable.add, memLp_trim_of_mem_lpMeasSubgroup, ProbabilityTheory.stronglyMeasurable_exponentialPDFReal, ProbabilityTheory.stronglyMeasurable_condVar, stronglyMeasurable_stoppedValue_of_le, StronglyMeasurable.Finset.stronglyMeasurable_sum_apply, Filtration.stronglyMeasurable_limitProcess, StronglyMeasurable.const_vadd, StronglyMeasurable.star, StronglyMeasurable.const_smul', StronglyMeasurable.of_uncurry_left

MeasureTheory.StronglyMeasurable

Theorems

NameKindAssumesProvesValidatesDepends On
limUnder 📖mathematicalMeasureTheory.StronglyMeasurableMeasureTheory.StronglyMeasurable
Filter.limUnder
Filter.eq_or_neBot
Filter.lim.congr_simp
Filter.map_bot
MeasureTheory.stronglyMeasurable_const
stronglyMeasurable_iff_measurable_separable
TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace
TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace
measurableSet_exists_tendsto
Function.extend_val_apply
Function.extend_val_apply'
limUnder_of_not_tendsto
MeasurableEmbedding.measurable_extend
MeasurableEmbedding.subtype_coe
measurable_of_tendsto_metrizable'
Measurable.comp
measurable
measurable_subtype_coe
tendsto_pi_nhds
Filter.Tendsto.limUnder_eq
TopologicalSpace.t2Space_of_metrizableSpace
measurable_const
TopologicalSpace.IsSeparable.union
TopologicalSpace.IsSeparable.closure
TopologicalSpace.IsSeparable.iUnion
isSeparable_range
Set.Finite.isSeparable
Set.finite_singleton
TopologicalSpace.IsSeparable.mono
Set.subset_union_left
mem_closure_of_tendsto
Filter.Eventually.of_forall
Set.mem_iUnion
Set.subset_union_right
Set.mem_singleton
measurableSet_exists_tendsto 📖mathematicalMeasureTheory.StronglyMeasurableMeasurableSet
setOf
Filter.Tendsto
nhds
Filter.eq_or_neBot
UniformSpace.secondCountable_of_separable
instIsCountablyGeneratedProdElemUniformity
EMetric.instIsCountablyGeneratedUniformity
TopologicalSpace.IsSeparable.separableSpace
PseudoEMetricSpace.pseudoMetrizableSpace
TopologicalSpace.IsSeparable.closure
TopologicalSpace.IsSeparable.iUnion
isSeparable_range
IsClosed.isCompletelyMetrizableSpace
isClosed_closure
subset_closure
Set.mem_iUnion
measurable
mem_closure_of_tendsto
Filter.Eventually.of_forall
tendsto_subtype_rng
MeasureTheory.measurableSet_exists_tendsto
Subtype.opensMeasurableSpace
BorelSpace.opensMeasurable

---

← Back to Index