Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ (x y : Ω →ᵇ ℝ≥0), dist (testAgainstNN μ x) (testAgainstNN μ y) ≤ ↑(mass μ) * dist x y
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ LipschitzWith (mass μ) fun f => testAgainstNN μ f
rw [lipschitzWith_iff_dist_le_mul]
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ dist (testAgainstNN μ f₁) (testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ (x y : Ω →ᵇ ℝ≥0), dist (testAgainstNN μ x) (testAgainstNN μ y) ≤ ↑(mass μ) * dist x y
intro f₁ f₂
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ abs (↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)) ≤ ↑(mass μ) * dist f₁ f₂
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ dist (testAgainstNN μ f₁) (testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
suffices abs (μ.testAgainstNN f₁ - μ.testAgainstNN f₂ : ℝ) ≤ μ.mass * dist f₁ f₂ by
  rwa [NNReal.dist_eq]
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ∧
    ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ abs (↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)) ≤ ↑(mass μ) * dist f₁ f₂
apply abs_le.mpr
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)

case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ∧
    ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
constructor
no goals
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
this : abs (↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)) ≤ ↑(mass μ) * dist f₁ f₂
⊢ dist (testAgainstNN μ f₁) (testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
rwa [NNReal.dist_eq]
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + nndist f₂ f₁ * mass μ
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
have key' := μ.testAgainstNN_lipschitz_estimate f₂ f₁
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + nndist f₂ f₁ * mass μ
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
rw [mul_comm] at key'
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
⊢ ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁) + ↑(mass μ) * dist f₁ f₂
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
suffices ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂ by linarith
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
key : ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁ + mass μ * nndist f₂ f₁)
⊢ ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁) + ↑(mass μ) * dist f₁ f₂
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
⊢ ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁) + ↑(mass μ) * dist f₁ f₂
have key := NNReal.coe_mono key'
no goals
case left
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
key : ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁ + mass μ * nndist f₂ f₁)
⊢ ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁) + ↑(mass μ) * dist f₁ f₂
rwa [NNReal.coe_add, NNReal.coe_mul, nndist_comm] at key
no goals
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₂ ≤ testAgainstNN μ f₁ + mass μ * nndist f₂ f₁
this : ↑(testAgainstNN μ f₂) ≤ ↑(testAgainstNN μ f₁) + ↑(mass μ) * dist f₁ f₂
⊢ -(↑(mass μ) * dist f₁ f₂) ≤ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂)
linarith
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + nndist f₁ f₂ * mass μ
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
have key' := μ.testAgainstNN_lipschitz_estimate f₁ f₂
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + nndist f₁ f₂ * mass μ
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
rw [mul_comm] at key'
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
⊢ ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂) + ↑(mass μ) * dist f₁ f₂
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
suffices ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂ by linarith
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
key : ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂ + mass μ * nndist f₁ f₂)
⊢ ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂) + ↑(mass μ) * dist f₁ f₂
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
⊢ ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂) + ↑(mass μ) * dist f₁ f₂
have key := NNReal.coe_mono key'
no goals
case right
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
key : ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂ + mass μ * nndist f₁ f₂)
⊢ ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂) + ↑(mass μ) * dist f₁ f₂
rwa [NNReal.coe_add, NNReal.coe_mul] at key
no goals
Ω : Type u_1
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.82801
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key' : testAgainstNN μ f₁ ≤ testAgainstNN μ f₂ + mass μ * nndist f₁ f₂
this : ↑(testAgainstNN μ f₁) ≤ ↑(testAgainstNN μ f₂) + ↑(mass μ) * dist f₁ f₂
⊢ ↑(testAgainstNN μ f₁) - ↑(testAgainstNN μ f₂) ≤ ↑(mass μ) * dist f₁ f₂
linarith