mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᵐ[μ] fun x ↦ ‖f‖

Tactic:
·

Goal state after:
α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ⇑f ≤ᵐ[μ] fun x ↦ ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ (ν (thickening ε {a | t ≤ f a})).toReal + ε =
    (ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε).toReal

pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ∞

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ (ν (thickening ε {a | t ≤ f a})).toReal + ε =
    (ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε).toReal
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ∞

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ∞
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ⊆ u

Tactic:
·

Goal state after:
case h.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ⊆ u
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
⊢ AEStronglyMeasurable (fun t ↦ μ.real {a | t ≤ f a}) volume

pp: case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖μ.real {a_1 | a ≤ f a_1}‖ ≤ μ.real univ

Tactic:
·

Goal state after:
case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
⊢ AEStronglyMeasurable (fun t ↦ μ.real {a | t ≤ f a}) volume
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖μ.real {a_1 | a ≤ f a_1}‖ ≤ μ.real univ

Tactic:
·

Goal state after:
case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖μ.real {a_1 | a ≤ f a_1}‖ ≤ μ.real univ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ AEStronglyMeasurable (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) volume

pp: case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖ν.real (thickening ε {a_1 | a ≤ f a_1})‖ ≤ ν.real univ

Tactic:
·

Goal state after:
case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ AEStronglyMeasurable (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) volume
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖ν.real (thickening ε {a_1 | a ≤ f a_1})‖ ≤ ν.real univ

Tactic:
·

Goal state after:
case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖ν.real (thickening ε {a_1 | a ≤ f a_1})‖ ≤ ν.real univ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: case h'
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) := ⋯
this : IsPiSystem S
⊢ ∀ s ∈ S, Tendsto (fun i ↦ (pi i) s) (𝓝 μ) (𝓝 (((fun μ ↦ pi μ) μ) s))

Tactic:
·

Goal state after:
case h'
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) := ⋯
this : IsPiSystem S
⊢ ∀ s ∈ S, Tendsto (fun i ↦ (pi i) s) (𝓝 μ) (𝓝 (((fun μ ↦ pi μ) μ) s))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ ∫ (x : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | x ≤ f a}) + ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume

pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ ∫ (x : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | x ≤ f a}) + ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ (∫ (a : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a_1 | a ≤ f a_1})) + ∫ (a : ℝ) in Ioc 0 ‖f‖, ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

pp: case hf
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ν.real (thickening ε {a | x ≤ f a})) (volume.restrict (Ioc 0 ‖f‖))

pp: case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ (∫ (a : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a_1 | a ≤ f a_1})) + ∫ (a : ℝ) in Ioc 0 ‖f‖, ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case hf
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ν.real (thickening ε {a | x ≤ f a})) (volume.restrict (Ioc 0 ‖f‖))

pp: case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
·

Goal state after:
case hf
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ν.real (thickening ε {a | x ≤ f a})) (volume.restrict (Ioc 0 ‖f‖))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
·

Goal state after:
case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
⊢ ∫ (x : X), f x ∂rieszMeasure Λ ≤ Λ f

pp: case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
⊢ Λ f ≤ ∫ (x : X), f x ∂rieszMeasure Λ

Tactic:
·

Goal state after:
case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
⊢ ∫ (x : X), f x ∂rieszMeasure Λ ≤ Λ f
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume

pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
·

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) (Ioc 0 ‖f‖) volume