Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ) ≤ ∫⁻ (ω : Ω), ↑(↑g ω) + edist f g ∂↑μ
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ testAgainstNN μ f ≤ testAgainstNN μ g + nndist f g * mass μ
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]
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (fun a => ↑(↑f a)) ≤ fun a => ↑(↑g a) + edist f g
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ) ≤ ∫⁻ (ω : Ω), ↑(↑g ω) + edist f g ∂↑μ
apply lintegral_mono
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ (fun a => ↑(↑f a)) ≤ fun a => ↑(↑g a) + edist f g
have le_dist : ∀ ω, dist (f ω) (g ω) ≤ nndist f g := BoundedContinuousFunction.dist_coe_le_dist
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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
intro ω
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
have le' : f ω ≤ g ω + nndist f g := by
  apply (NNReal.le_add_nndist (f ω) (g ω)).trans
  rw [add_le_add_iff_left]
  exact dist_le_coe.mp (le_dist ω)
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
have le : (f ω : ℝ≥0∞) ≤ (g ω : ℝ≥0∞) + nndist f g := by
  rw [← ENNReal.coe_add];
  exact ENNReal.coe_mono le'
no goals
case hfg
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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) ω
rwa [coe_nnreal_ennreal_nndist] at le
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (↑f ω) (↑g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ ↑g ω + nndist (↑f ω) (↑g ω) ≤ ↑g ω + nndist f g
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (↑f ω) (↑g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ ↑f ω ≤ ↑g ω + nndist f g
apply (NNReal.le_add_nndist (f ω) (g ω)).trans
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (↑f ω) (↑g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ nndist (↑f ω) (↑g ω) ≤ nndist f g
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (↑f ω) (↑g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ ↑g ω + nndist (↑f ω) (↑g ω) ≤ ↑g ω + nndist f g
rw [add_le_add_iff_left]
no goals
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (↑f ω) (↑g ω) ≤ ↑(nndist f g)
ω : Ω
⊢ nndist (↑f ω) (↑g ω) ≤ nndist f g
exact dist_le_coe.mp (le_dist ω)
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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)
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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)
rw [← ENNReal.coe_add]
no goals
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.76875
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
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)
exact ENNReal.coe_mono le'