Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
E_nullbdry' : ↑↑↑μ (frontier E) = 0
⊢ Tendsto (fun i => (fun s => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (𝓝 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) E))
Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
⊢ Tendsto (fun i => (fun s => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (𝓝 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) E))
have E_nullbdry' : (μ : Measure Ω) (frontier E) = 0 := by
  rw [← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, E_nullbdry, ENNReal.coe_zero]
Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
E_nullbdry' : ↑↑↑μ (frontier E) = 0
key : Tendsto (fun i => ↑↑↑(μs i) E) L (𝓝 (↑↑↑μ E))
⊢ Tendsto (fun i => (fun s => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (𝓝 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) E))
Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
E_nullbdry' : ↑↑↑μ (frontier E) = 0
⊢ Tendsto (fun i => (fun s => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (𝓝 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) E))
have key := ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' μs_lim E_nullbdry'
no goals
Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
E_nullbdry' : ↑↑↑μ (frontier E) = 0
key : Tendsto (fun i => ↑↑↑(μs i) E) L (𝓝 (↑↑↑μ E))
⊢ Tendsto (fun i => (fun s => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (𝓝 ((fun s => ENNReal.toNNReal (↑↑↑μ s)) E))
exact (ENNReal.tendsto_toNNReal (measure_ne_top (↑μ) E)).comp key
no goals
Ω✝ : Type ?u.40691
inst✝³ : MeasurableSpace Ω✝
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : (fun s => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0
⊢ ↑↑↑μ (frontier E) = 0
rw [← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, E_nullbdry, ENNReal.coe_zero]