-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_lipschitz_estimate (μ : FiniteMeasure Ω) (f g : Ω →ᵇ ℝ≥0) :
    μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass

Proof state:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g

Tactic:
have le_dist : ∀ ω, dist (f ω) (g ω) ≤ nndist f g := BoundedContinuousFunction.dist_coe_le_dist

Result:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
⊢ (fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ ↑(f ω) ≤ ↑(g ω + nndist f g)

Tactic:
exact_mod_cast le'

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass

Tactic:
simp only [← μ.testAgainstNN_const (nndist f g), ← testAgainstNN_add, ← ENNReal.coe_le_coe,
  BoundedContinuousFunction.coe_add, const_apply, ENNReal.coe_add, Pi.add_apply,
  coe_nnreal_ennreal_nndist, testAgainstNN_coe_eq]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) + edist f g ∂↑μ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ f ω ≤ g ω + nndist f g

Tactic:
calc f ω
 _ ≤ g ω + nndist (f ω) (g ω)     := NNReal.le_add_nndist (f ω) (g ω)
 _ ≤ g ω + nndist f g             := (add_le_add_iff_left (g ω)).mpr (le_dist ω)

Result:
no goals

Proof state:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
⊢ (fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g

Tactic:
intro ω

Result:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ ↑(f ω) ≤ ↑(g ω) + ↑(nndist f g)

Tactic:
simpa only [← ENNReal.coe_add] using (by exact_mod_cast le')

Result:
no goals

Proof state:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
le : ↑(f ω) ≤ ↑(g ω) + ↑(nndist f g)
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω

Tactic:
rwa [coe_nnreal_ennreal_nndist] at le

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) + edist f g ∂↑μ

Tactic:
apply lintegral_mono

Result:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g

Proof state:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω

Tactic:
have le : (f ω : ℝ≥0∞) ≤ (g ω : ℝ≥0∞) + nndist f g := by
  simpa only [← ENNReal.coe_add] using (by exact_mod_cast le')

Result:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
le : ↑(f ω) ≤ ↑(g ω) + ↑(nndist f g)
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω

Proof state:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω

Tactic:
have le' : f ω ≤ g ω + nndist f g := by
  calc f ω
   _ ≤ g ω + nndist (f ω) (g ω)     := NNReal.le_add_nndist (f ω) (g ω)
   _ ≤ g ω + nndist f g             := (add_le_add_iff_left (g ω)).mpr (le_dist ω)

Result:
case hfg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)
ω : Ω
le' : f ω ≤ g ω + nndist f g
⊢ (fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω