ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<GOAL>ContinuousAt toLevyProkhorov P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<GOAL>∀ ε > 0, ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<GOAL>∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist x.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : Q ∈ ⋂ i ∈ Js_finite.toFinset, {Q | ↑P (thickening (ε / 3) (⋃ j ∈ i, Es j)) < ↑Q (thickening (ε / 3) (⋃ j ∈ i, Es j)) + ENNReal.ofReal (ε / 3)}<GOAL>dist Q.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<GOAL>dist Q.toLevyProkhorov P.toLevyProkhorov < ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<GOAL>dist Q.toLevyProkhorov P.toLevyProkhorov ≤ 2 * (ε / 3)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<GOAL>dist P.toLevyProkhorov Q.toLevyProkhorov ≤ 2 * (ε / 3)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<GOAL>↑P.toLevyProkhorov B ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<GOAL>↑P.toLevyProkhorov B ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<GOAL>↑P.toLevyProkhorov B ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ∀ i ⊆ Iio N, ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<GOAL>↑P.toLevyProkhorov (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ↑P.toLevyProkhorov (⋃ j ∈ Iio N, Es j)ᶜ ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<VAR>hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)<GOAL>↑P.toLevyProkhorov (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ↑P.toLevyProkhorov (⋃ j ∈ Iio N, Es j)ᶜ ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<VAR>hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)<GOAL>↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3) + ENNReal.ofReal (ε / 3) ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<VAR>hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)<GOAL>↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (2 * (ε / 3)) ≤ ↑Q.toLevyProkhorov (thickening δ B) + ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>third_ε_pos : 0 < ε / 3<VAR>third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)<VAR>Es : ℕ → Set Ω<VAR>Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)<VAR>Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)<VAR>Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3<VAR>Es_cover : ⋃ n, Es n = univ<VAR>Es_disjoint : Pairwise fun n m => Disjoint (Es n) (Es m)<VAR>N : ℕ<VAR>hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)<VAR>Js_finite : {J | J ⊆ Iio N}.Finite<VAR>Gs : Set (Set Ω) := (fun J => thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}<VAR>Gs_open : ∀ (J : Set ℕ), IsOpen (thickening (ε / 3) (⋃ j ∈ J, Es j))<VAR>mem_nhds_P : ∀ (G : Set Ω), IsOpen G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P<VAR>Q : ProbabilityMeasure Ω<VAR>δ : ℝ<VAR>B : Set Ω<VAR>δ_gt : 2 * (ε / 3) < δ<VAR>x✝ : MeasurableSet B<VAR>JB : Set ℕ := {i | B ∩ Es i ≠ ∅ ∧ i ∈ Iio N}<VAR>B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ<VAR>subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B<VAR>hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)<GOAL>2 * (ε / 3) ≤ δ
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>j : Fin (n + 1)<GOAL>j ∈ c.toComposition.boundaries ↔ j ∈ c.boundaries
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>j : Fin (n + 1)<GOAL>(∃ a ∈ Finset.univ, c.toComposition.boundary.toEmbedding a = j) ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : IsRightCancelMulZero α<VAR>x y : α<VAR>h : x * y = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<GOAL>Disjoint (f.genEigenrange μ (finrank K V)) ((f.genEigenspace μ) (finrank K V))
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : Submodule.comap ((f - (algebraMap K (End K V)) μ) ^ finrank K V) ((f.genEigenspace μ) (finrank K V)) = (f.genEigenspace μ) (finrank K V)<GOAL>Disjoint (f.genEigenrange μ (finrank K V)) ((f.genEigenspace μ) (finrank K V))
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : Submodule.comap ((f - (algebraMap K (End K V)) μ) ^ finrank K V) ((f.genEigenspace μ) (finrank K V)) = (f.genEigenspace μ) (finrank K V)<GOAL>Submodule.map ((f - (algebraMap K (End K V)) μ) ^ finrank K V) ((f.genEigenspace μ) (finrank K V)) ≤ ⊥
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<GOAL>x.denom.Monic