ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>g : G<GOAL>μ {g} = μ {0}
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>c : ℝ≥0∞<VAR>cpos : c ≠ 0<VAR>ctop : c ≠ ⊤<GOAL>(c • μ).IsHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>c : ℝ≥0∞<VAR>cpos : c ≠ 0<VAR>ctop : c ≠ ⊤<GOAL>(c • μ).IsAddHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h'K : (interior K).Nonempty<VAR>h : μ K ≠ 0<VAR>h' : μ K ≠ ⊤<GOAL>μ.IsHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h'K : (interior K).Nonempty<VAR>h : μ K ≠ 0<VAR>h' : μ K ≠ ⊤<GOAL>μ.IsAddHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>BorelSpace G<VAR>TopologicalGroup G<VAR>H : Type u_4<VAR>Group H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>T2Space H<VAR>TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>h_surj : Function.Surjective ⇑f<VAR>h_prop : Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H)<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>BorelSpace G<VAR>TopologicalAddGroup G<VAR>H : Type u_4<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>T2Space H<VAR>TopologicalAddGroup H<VAR>f : G →+ H<VAR>hf : Continuous ⇑f<VAR>h_surj : Function.Surjective ⇑f<VAR>h_prop : Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H)<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>BorelSpace G<VAR>TopologicalGroup G<VAR>H : Type u_4<VAR>Group H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>TopologicalGroup H<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>h_surj : Function.Surjective ⇑f<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>BorelSpace G<VAR>TopologicalAddGroup G<VAR>H : Type u_4<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>TopologicalAddGroup H<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : G →+ H<VAR>hf : Continuous ⇑f<VAR>h_surj : Function.Surjective ⇑f<GOAL>(MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Group G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsHaarMeasure<VAR>BorelSpace G<VAR>TopologicalGroup G<VAR>H : Type u_4<VAR>Group H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>TopologicalGroup H<VAR>e : G ≃* H<VAR>he : Continuous ⇑e<VAR>hesymm : Continuous ⇑e.symm<GOAL>(MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddHaarMeasure<VAR>BorelSpace G<VAR>TopologicalAddGroup G<VAR>H : Type u_4<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>MeasurableSpace H<VAR>BorelSpace H<VAR>TopologicalAddGroup H<VAR>e : G ≃+ H<VAR>he : Continuous ⇑e<VAR>hesymm : Continuous ⇑e.symm<GOAL>(MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup E<VAR>Module R E<VAR>AddCommGroup F<VAR>Module S F<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>L : E ≃SL[σ] F<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<GOAL>(MeasureTheory.Measure.map (⇑L) μ).IsAddHaarMeasure
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CommSemiring A<VAR>z : E<VAR>NormedRing B<VAR>NormedAlgebra 𝕜 B<VAR>Algebra A B<VAR>f : E → B<VAR>hf : AnalyticAt 𝕜 f z<VAR>p : Polynomial A<GOAL>AnalyticAt 𝕜 (fun x => (Polynomial.aeval (f x)) p) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CommSemiring A<VAR>s : Set E<VAR>NormedRing B<VAR>NormedAlgebra 𝕜 B<VAR>Algebra A B<VAR>f : E → B<VAR>hf : AnalyticOn 𝕜 f s<VAR>p : Polynomial A<GOAL>AnalyticOn 𝕜 (fun x => (Polynomial.aeval (f x)) p) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_5<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>p : Polynomial A<GOAL>AnalyticOn 𝕜 (fun x => Polynomial.eval x p) Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CommSemiring A<VAR>z : E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z<VAR>p : MvPolynomial σ A<GOAL>AnalyticAt 𝕜 (fun x => (MvPolynomial.aeval (f x)) p) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CommSemiring A<VAR>s : Set E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticOn 𝕜 (fun x => f x i) s<VAR>p : MvPolynomial σ A<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.aeval (f x)) p) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>σ : Type u_5<VAR>f : E →L[𝕜] σ → B<VAR>p : MvPolynomial σ B<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.eval (f x)) p) Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>σ : Type u_5<VAR>f : σ → E →L[𝕜] B<VAR>p : MvPolynomial σ B<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.eval fun x_1 => (f x_1) x) p) Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>σ : Type u_5<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] σ → B<VAR>p : MvPolynomial σ B<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.eval (f x)) p) Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>B : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedCommRing B<VAR>NormedAlgebra 𝕜 B<VAR>σ : Type u_5<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : σ → E →ₗ[𝕜] B<VAR>p : MvPolynomial σ B<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.eval fun x_1 => (f x_1) x) p) Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>σ : Type u_5<VAR>CompleteSpace 𝕜<VAR>Fintype σ<VAR>p : MvPolynomial σ 𝕜<GOAL>AnalyticOn 𝕜 (fun x => (MvPolynomial.eval x) p) Set.univ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure Ω<VAR>h_le : ε₁ ≤ ε₂<VAR>B : Set Ω<VAR>hε₁ : μ B ≤ ν (Metric.thickening ε₁.toReal B) + ε₁<GOAL>μ B ≤ ν (Metric.thickening ε₂.toReal B) + ε₂
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>c : ℝ≥0∞<VAR>h : MeasureTheory.levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<GOAL>μ B ≤ ν (Metric.thickening c.toReal B) + c
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>c : ℝ≥0∞<VAR>h : MeasureTheory.levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<GOAL>ν B ≤ μ (Metric.thickening c.toReal B) + c
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (Metric.thickening (δ + ε).toReal B) + δ + ε<GOAL>MeasureTheory.levyProkhorovEDist μ ν ≤ δ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε ∧ ν B ≤ μ (Metric.thickening ε.toReal B) + ε<GOAL>MeasureTheory.levyProkhorovEDist μ ν ≤ δ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovEDist μ ν ≤ max (μ Set.univ) (ν Set.univ)
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>MeasureTheory.levyProkhorovEDist μ ν < ⊤
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>MeasureTheory.levyProkhorovEDist μ ν ≠ ⊤
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovEDist μ μ = 0
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovEDist μ ν = MeasureTheory.levyProkhorovEDist ν μ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν κ : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovEDist μ κ ≤ MeasureTheory.levyProkhorovEDist μ ν + MeasureTheory.levyProkhorovEDist ν κ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovDist μ μ = 0
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<GOAL>MeasureTheory.levyProkhorovDist μ ν = MeasureTheory.levyProkhorovDist ν μ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν κ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>MeasureTheory.IsFiniteMeasure κ<GOAL>MeasureTheory.levyProkhorovDist μ κ ≤ MeasureTheory.levyProkhorovDist μ ν + MeasureTheory.levyProkhorovDist ν κ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω)<GOAL>dist μ ν = MeasureTheory.levyProkhorovDist ↑μ ↑ν
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure ν<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε<GOAL>MeasureTheory.levyProkhorovEDist μ ν ≤ δ
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure ν<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (Metric.thickening ε B) + ENNReal.ofReal ε<GOAL>MeasureTheory.levyProkhorovDist μ ν ≤ δ
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>f : BoundedContinuousFunction α ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] ⇑f<VAR>hf : MeasureTheory.HasFiniteIntegral (⇑f) μ<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>TopologicalSpace α<VAR>OpensMeasurableSpace α<VAR>f : BoundedContinuousFunction α ℝ<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f_nn : 0 ≤ᵐ[μ] ⇑f<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : MeasureTheory.levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : BoundedContinuousFunction Ω ℝ<VAR>f_nn : 0 ≤ᵐ[μ] ⇑f<GOAL>∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Set.Ioc 0 ‖f‖, (ν (Metric.thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>f : BoundedContinuousFunction Ω ℝ<VAR>A : Set ℝ<VAR>A_finmeas : MeasureTheory.volume A ≠ ⊤<VAR>μ : MeasureTheory.ProbabilityMeasure Ω<GOAL>Filter.Tendsto (fun ε => ∫ (t : ℝ) in A, (↑(μ (Metric.thickening ε {a | t ≤ f a}))).toReal) (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in A, (↑(μ {a | t ≤ f a})).toReal))
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoMetricSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous MeasureTheory.LevyProkhorov.toProbabilityMeasure
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoMetricSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>TopologicalSpace.coinduced MeasureTheory.LevyProkhorov.toProbabilityMeasure inferInstance ≤ inferInstance
<VAR>Ω : Type u_2<VAR>PseudoMetricSpace Ω<VAR>TopologicalSpace.SeparableSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>∃ As, (∀ (n : ℕ), MeasurableSet (As n)) ∧ (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧ (∀ (n : ℕ), Metric.diam (As n) ≤ ε) ∧ ⋃ n, As n = Set.univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
<VAR>Ω : Type u_2<VAR>PseudoMetricSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>P : MeasureTheory.ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<GOAL>{Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P
<VAR>Ω : Type u_2<VAR>PseudoMetricSpace Ω<VAR>TopologicalSpace.SeparableSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>Continuous MeasureTheory.ProbabilityMeasure.toLevyProkhorov
<VAR>Ω : Type u_2<VAR>PseudoMetricSpace Ω<VAR>TopologicalSpace.SeparableSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<GOAL>inferInstance = TopologicalSpace.coinduced MeasureTheory.LevyProkhorov.toProbabilityMeasure inferInstance
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<GOAL>Set.EqOn f 0 U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<GOAL>Set.EqOn f 0 U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfg : f =ᶠ[𝓝 z₀] g<GOAL>Set.EqOn f g U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>PreconnectedSpace E<VAR>hf : AnalyticOn 𝕜 f Set.univ<VAR>hg : AnalyticOn 𝕜 g Set.univ<VAR>z₀ : E<VAR>hfg : f =ᶠ[𝓝 z₀] g<GOAL>f = g
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>self : MeasureTheory.JordanDecomposition α<GOAL>self.posPart ⟂ₘ self.negPart
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>self : MeasureTheory.JordanDecomposition α<GOAL>MeasureTheory.IsFiniteMeasure self.negPart
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>self : MeasureTheory.JordanDecomposition α<GOAL>MeasureTheory.IsFiniteMeasure self.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.JordanDecomposition.posPart 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.JordanDecomposition.negPart 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>(-j).posPart = j.negPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>(-j).negPart = j.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ≥0<GOAL>(r • j).posPart = r • j.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ≥0<GOAL>(r • j).negPart = r • j.negPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>r : ℝ<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ≥0<GOAL>↑r • j = r • j
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>r • j = r.toNNReal • j
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : r < 0<GOAL>r • j = -((-r).toNNReal • j)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(r • j).posPart = r.toNNReal • j.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(r • j).negPart = r.toNNReal • j.negPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : r < 0<GOAL>(r • j).posPart = (-r).toNNReal • j.negPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ<VAR>hr : r < 0<GOAL>(r • j).negPart = (-r).toNNReal • j.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.JordanDecomposition.toSignedMeasure 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>(-j).toSignedMeasure = -j.toSignedMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>r : ℝ≥0<GOAL>(r • j).toSignedMeasure = r • j.toSignedMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>∃ S, MeasurableSet S ∧ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S ≤ MeasureTheory.VectorMeasure.restrict 0 S ∧ MeasureTheory.VectorMeasure.restrict 0 Sᶜ ≤ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>∃ i, ∃ (hi₁ : MeasurableSet i) (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₃ : MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>s.toJordanDecomposition.toSignedMeasure = s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u<VAR>hsv : MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v<VAR>hs : ↑s (symmDiff u v) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u<VAR>hsv : MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v<VAR>hs : ↑s (symmDiff u v) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u<VAR>hsv : MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v<VAR>hs : ↑s (symmDiff u v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u<VAR>hsv : MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v<VAR>hs : ↑s (symmDiff u v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j₁ j₂ : MeasureTheory.JordanDecomposition α<VAR>hj : j₁.posPart = j₂.posPart<VAR>hj' : j₁.toSignedMeasure = j₂.toSignedMeasure<GOAL>j₁ = j₂
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>j.toSignedMeasure.toJordanDecomposition = j
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>j : MeasureTheory.JordanDecomposition α<GOAL>(MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α).symm j = j.toSignedMeasure
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>(MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α) s = s.toJordanDecomposition
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.SignedMeasure.toJordanDecomposition 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>(-s).toJordanDecomposition = -s.toJordanDecomposition
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>r : ℝ≥0<GOAL>(r • s).toJordanDecomposition = r • s.toJordanDecomposition
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(r • s).toJordanDecomposition = r • s.toJordanDecomposition
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>r : ℝ<GOAL>(r • s).toJordanDecomposition = r • s.toJordanDecomposition
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>j : MeasureTheory.JordanDecomposition α<VAR>h : s = j.toSignedMeasure<GOAL>s.toJordanDecomposition = j
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.SignedMeasure.totalVariation 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>(-s).totalVariation = s.totalVariation
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hs : s.totalVariation i = 0<GOAL>↑s i = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ