case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : p = 0
⊢ snorm (Set.indicator s (f - g)) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)

case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
⊢ snorm (Set.indicator s (f - g)) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
⊢ snorm (Set.indicator s (f - g)) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
by_cases hp : p = 0
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ snorm (fun x => Set.indicator s (fun x => c) x) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ snorm (Set.indicator s (f - g)) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
refine' le_trans (snorm_mono this) _
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ snorm (fun x => Set.indicator s (fun x => c) x) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
rw [snorm_indicator_const hs hp hp']
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ ↑‖c‖₊ = ENNReal.ofReal c
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
refine' mul_le_mul_right' (le_of_eq _) _
no goals
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
⊢ ↑‖c‖₊ = ENNReal.ofReal c
rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_eq_abs, abs_of_nonneg hc]
no goals
case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : p = 0
⊢ snorm (Set.indicator s (f - g)) p μ ≤ ENNReal.ofReal c * ↑↑μ s ^ (1 / ENNReal.toReal p)
simp [hp]
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
⊢ ∀ (x : α), ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
intro x
case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖

case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : ¬x ∈ s
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
by_cases hx : x ∈ s
case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ c
case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
  Real.norm_eq_abs, abs_of_nonneg hc]
no goals
case pos
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ c
exact hf x hx
no goals
case neg
α : Type u_1
β : Type u_2
ι : Type ?u.346477
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p✝ p : ℝ≥0∞
hp' : p ≠ ⊤
s : Set α
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ (x : α), x ∈ s → dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : ¬x ∈ s
⊢ ‖Set.indicator s (f - g) x‖ ≤ ‖Set.indicator s (fun x => c) x‖
simp [Set.indicator_of_not_mem hx]