📁 Source: Mathlib/MeasureTheory/Measure/Prokhorov.lean
instCompactSpaceProbabilityMeasure
isCompact_closure_of_isTightMeasureSet
isCompact_setOf_finiteMeasure_eq_of_compactSpace
isCompact_setOf_finiteMeasure_le_of_compactSpace
isCompact_setOf_finiteMeasure_le_of_isCompact
isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le
isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le
isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le
CompactSpace
MeasureTheory.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.instTopologicalSpace
BorelSpace.opensMeasurable
Topology.IsEmbedding.isCompact_iff
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding
Set.image_univ
MeasureTheory.ProbabilityMeasure.range_toFiniteMeasure
MeasureTheory.IsTightMeasureSet
setOf
MeasureTheory.Measure
Set
Set.instMembership
MeasureTheory.ProbabilityMeasure.toMeasure
IsCompact
closure
exists_seq_strictAnti_tendsto
NNReal.instOrderTopology
NNReal.instDenselyOrdered
IsStrictOrderedRing.toNoMaxOrder
NNReal.instIsStrictOrderedRing
TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology
PseudoEMetricSpace.pseudoMetrizableSpace
MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le
Nat.cast_zero
ENNReal.coe_le_coe
MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure
Set.Finite.isCompact_biUnion
Set.finite_Iic
Set.iUnion_congr_Prop
Set.subset_biUnion_of_mem
LE.le.trans
IsCompact.closure_of_subset
MeasureTheory.ProbabilityMeasure.R1Space
MeasureTheory.ProbabilityMeasure.apply_mono
Set.compl_subset_compl_of_subset
le_rfl
MeasureTheory.FiniteMeasure
MeasureTheory.FiniteMeasure.instTopologicalSpace
NNReal
MeasureTheory.FiniteMeasure.mass
IsCompact.inter_right
isClosed_eq
TopologicalSpace.t2Space_of_metrizableSpace
EMetricSpace.metrizableSpace
MeasureTheory.FiniteMeasure.continuous_mass
continuous_const
Preorder.toLE
PartialOrder.toPreorder
instPartialOrderNNReal
isCompact_iff_ultrafilter_le_nhds'
IsCompact.ultrafilter_le_nhds'
CompactIccSpace.isCompact_Icc
ConditionallyCompleteLinearOrder.toCompactIccSpace
instOrderTopologyReal
neg_mul
Filter.mp_mem
Filter.univ_mem'
MeasureTheory.integral_const
Real.instCompleteSpace
mul_neg
IsOrderedAddMonoid.toAddLeftMono
Real.instIsOrderedAddMonoid
covariant_swap_add_of_covariant_add
mul_le_mul_of_nonneg_right
IsOrderedRing.toMulPosMono
Real.instIsOrderedRing
norm_nonneg
MeasureTheory.integral_mono
IsStrictOrderedModule.toIsOrderedModule
IsStrictOrderedRing.toIsStrictOrderedModule
Real.instIsStrictOrderedRing
instClosedIciTopology
HasSolidNorm.orderClosedTopology
instHasSolidNormReal
MeasureTheory.FiniteMeasure.isFiniteMeasure
enorm_neg
enorm_norm
Continuous.integrable_of_hasCompactSupport
isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure
MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure
ContinuousMap.continuous
CompactlySupportedContinuousMap.hasCompactSupport
neg_le_of_abs_le
BoundedContinuousFunction.norm_coe_le_norm
le_of_abs_le
IsTopologicalSemiring.toContinuousAdd
IsTopologicalRing.toIsTopologicalSemiring
instIsTopologicalRingReal
UniformContinuousConstSMul.to_continuousConstSMul
Ring.uniformContinuousConstSMul
instIsUniformAddGroupReal
IsTopologicalSemiring.toContinuousMul
MeasureTheory.integral_add
Filter.Tendsto.add
tendsto_nhds_unique
Ultrafilter.neBot
MeasureTheory.integral_smul
NormedSpace.toNormSMulClass
Algebra.to_smulCommClass
Filter.Tendsto.const_smul
le_of_tendsto_of_tendsto'
WeaklyLocallyCompactSpace.locallyCompactSpace
instR1Space
CompletelyRegularSpace.instRegularSpace
T35Space.toCompletelyRegularSpace
T4Space.instT35Space
T4Space.of_paracompactSpace_t2Space
paracompact_of_locallyCompact_sigmaCompact
instWeaklyLocallyCompactSpaceOfCompactSpace
CompactSpace.sigmaCompact
continuous_one
HasCompactSupport.of_compactSpace
RealRMK.rieszMeasure_le_of_eq_one
Real.instZeroLEOneClass
isCompact_univ
ENNReal.ofReal_le_ofReal
le_of_tendsto
instClosedIicTopology
mul_one
LE.le.trans_lt
ENNReal.ofReal_coe_nnreal
ENNReal.toNNReal_mono
MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto
ContinuousMapClass.map_continuous
BoundedContinuousMapClass.toContinuousMapClass
BoundedContinuousFunction.instBoundedContinuousMapClass
RealRMK.integral_rieszMeasure
DFunLike.coe
MeasureTheory.FiniteMeasure.instFunLike
Compl.compl
Set.instCompl
instZeroNNReal
Topology.IsClosedEmbedding.subtypeVal
IsCompact.isClosed
Subtype.range_val
Set.Subset.antisymm
MeasureTheory.FiniteMeasure.mass_comap_le
MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq
MeasureTheory.Measure.map_apply
measurable_subtype_coe
MeasureTheory.Measure.comap_apply
Subtype.val_injective
MeasurableEmbedding.measurableSet_image'
Topology.IsClosedEmbedding.measurableEmbedding
Subtype.borelSpace
Continuous.measurable
Subtype.opensMeasurableSpace
Topology.IsClosedEmbedding.continuous
Set.image_preimage_eq_inter_range
MeasureTheory.Measure.restrict_apply
MeasureTheory.Measure.restrict_eq_self_of_ae_mem
MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
Set.image_congr
MeasurableSet.compl
IsCompact.measurableSet
MeasureTheory.FiniteMeasure.mass_map_le
Subtype.coe_preimage_self
Set.compl_univ
MeasureTheory.measure_empty
MeasureTheory.Measure.instOuterMeasureClass
IsCompact.image
isCompact_iff_compactSpace
instT2SpaceSubtype
MeasureTheory.FiniteMeasure.continuous_map
continuous_subtype_val
Filter.Tendsto
Filter.atTop
Nat.instPreorder
nhds
NNReal.instTopologicalSpace
NormalSpace
Monotone
OmegaCompletePartialOrder.toPartialOrder
CompleteLattice.instOmegaCompletePartialOrder
CompleteBooleanAlgebra.toCompleteLattice
CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra
Set.instCompleteAtomicBooleanAlgebra
Set.ext
biUnion_range_succ_disjointed
MeasureTheory.FiniteMeasure.restrict_biUnion_finset
Pairwise.set_pairwise
disjoint_disjointed
MeasurableSet.disjointed
Set.partialSups_eq_accumulate
isCompact_accumulate
Ultrafilter.coe_map
MeasureTheory.FiniteMeasure.restrict_mass
MeasureTheory.FiniteMeasure.apply_le_mass
disjoint_iff
Disjoint.mono_right
disjoint_compl_left
le_trans
sdiff_le
le_partialSups
MeasureTheory.Measure.exists_innerRegular_eq_of_isCompact
MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
MeasureTheory.Measure.sum_apply
Filter.Tendsto.comp
ENNReal.tendsto_nat_tsum
Filter.tendsto_add_atTop_nat
le_of_tendsto'
OrderTopology.to_orderClosedTopology
ENNReal.instOrderTopology
Filter.atTop_neBot
instIsDirectedOrder
IsStrictOrderedRing.toIsOrderedRing
Nat.instIsStrictOrderedRing
instArchimedeanNat
MeasureTheory.FiniteMeasure.toMeasure_sum
MeasureTheory.Measure.coe_finset_sum
Finset.sum_apply
Filter.Tendsto.mass
tendsto_finset_sum
MeasureTheory.FiniteMeasure.instContinuousAdd
MeasureTheory.FiniteMeasure.apply_mono
Set.subset_univ
MeasureTheory.FiniteMeasure.ennreal_mass
Metric.tendsto_nhds
Nat.instAtLeastTwoHAddOfNat
MeasureTheory.integral_sum_measure
BoundedContinuousFunction.integrable
instSecondCountableTopologyReal
Real.borelSpace
MeasureTheory.integral_finset_sum_measure
Summable.tendsto_sum_tsum_nat
HasSum.summable
MeasureTheory.hasSum_integral_measure
div_pos
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
Mathlib.Meta.Positivity.pos_of_isNat
Real.instNontrivial
Mathlib.Meta.NormNum.isNat_ofNat
Mathlib.Meta.NormNum.instAtLeastTwo
Filter.Tendsto.const_mul
NNReal.tendsto_coe
tendsto_order
MulZeroClass.mul_zero
Filter.Eventually.exists
Filter.Eventually.and
dist_triangle4
add_lt_add_of_lt_of_lt
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
AddLeftCancelSemigroup.toIsLeftCancelAdd
IsRightCancelAdd.addRightStrictMono_of_addRightMono
AddRightCancelSemigroup.toIsRightCancelAdd
MeasureTheory.FiniteMeasure.restrict_union
Set.compl_union_self
MeasureTheory.FiniteMeasure.restrict_univ
MeasureTheory.FiniteMeasure.toMeasure_add
MeasureTheory.integral_add_measure
dist_add_self_left
MeasureTheory.norm_integral_le_integral_norm
MeasureTheory.integral_mono_of_nonneg
MeasureTheory.isFiniteMeasureRestrict
MeasureTheory.measureReal_restrict_apply
Set.univ_inter
mul_comm
mul_le_mul_of_nonneg_left
IsOrderedRing.toPosMulMono
Finset.sum_congr
Mathlib.Tactic.Ring.of_eq
Mathlib.Tactic.Ring.add_congr
Mathlib.Tactic.Ring.div_congr
Mathlib.Tactic.Ring.atom_pf
Mathlib.Tactic.Ring.cast_pos
Mathlib.Tactic.Ring.div_pf
Mathlib.Tactic.Ring.inv_single
Mathlib.Meta.NormNum.IsNNRat.to_raw_eq
Mathlib.Meta.NormNum.isNNRat_inv_pos
RCLike.charZero_rclike
Mathlib.Meta.NormNum.IsNat.to_isNNRat
Mathlib.Meta.NormNum.IsNat.of_raw
Mathlib.Tactic.Ring.add_mul
Mathlib.Tactic.Ring.mul_add
Mathlib.Tactic.Ring.mul_pf_left
Mathlib.Tactic.Ring.one_mul
Mathlib.Tactic.Ring.mul_zero
Mathlib.Tactic.Ring.add_pf_add_zero
Mathlib.Tactic.Ring.zero_mul
Mathlib.Tactic.Ring.add_pf_add_overlap
Mathlib.Tactic.Ring.add_overlap_pf
Mathlib.Meta.NormNum.isNNRat_add
Mathlib.Meta.NormNum.IsNNRat.of_raw
Mathlib.Meta.NormNum.IsNNRat.den_nz
Mathlib.Tactic.Ring.add_pf_zero_add
Mathlib.Meta.NormNum.IsNat.to_raw_eq
Mathlib.Meta.NormNum.IsNNRat.to_isNat
MeasureTheory.Measure.InnerRegular.instSum_1
MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure
IsOpen.measure_eq_biSup_integral_continuous
IsClosed.isOpen_compl
MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop
iSup_congr_Prop
compl_compl
AddGroup.toOrderedSub
IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT
contravariant_swap_add_of_contravariant_add
contravariant_lt_of_covariant_le
IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT
MeasureTheory.Integrable.indicator
MeasureTheory.integrable_const
Set.indicator_of_mem
Set.indicator_of_notMem
le_of_eq
MeasureTheory.integral_indicator
Filter.Ici_mem_atTop
Finset.sum_subset
MeasureTheory.FiniteMeasure.mono_null
Monotone.partialSups_eq
Set.compl_subset_compl
biUnion_Ioc_disjointed_of_monotone
Set.diff_subset_compl
Finset.sum_le_sum
ENNReal.instIsOrderedAddMonoid
MeasureTheory.measure_mono
MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure
MeasureTheory.isProbabilityMeasure_iff_real
---
← Back to Index