-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem le_eLpNorm_of_bddBelow (hp : p ≠ 0) (hp' : p ≠ ∞) {f : α → F} (C : ℝ≥0) {s : Set α}
    (hs : MeasurableSet s) (hf : ∀ᵐ x ∂μ, x ∈ s → C ≤ ‖f x‖₊) :
    C • μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x => ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
refine lintegral_mono_ae ?_

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∀ᵐ (a : α) ∂μ, s.indicator (fun x => ↑C ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∀ᵐ (a : α) ∂μ, s.indicator (fun x => ↑C ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal

Tactic:
filter_upwards [hf] with x hx

Result:
case h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ ↑C ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
gcongr

Result:
case pos.h₁
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ ↑C ≤ ‖f x‖ₑ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∉ s
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
simp [Set.indicator_of_not_mem hxs]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
by_cases hxs : x ∈ s

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∈ s
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∉ s
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∈ s
⊢ s.indicator (fun x => ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
simp only [Set.indicator_of_mem, hxs, true_implies] at hx ⊢

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ ↑C ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ C • μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, eLpNorm_eq_lintegral_rpow_enorm hp hp',
  one_div, ENNReal.le_rpow_inv_iff (ENNReal.toReal_pos hp hp'),
  ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg, ← ENNReal.rpow_mul,
  inv_mul_cancel₀ (ENNReal.toReal_pos hp hp').ne.symm, ENNReal.rpow_one, ← setLIntegral_const,
  ← lintegral_indicator hs]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x => ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Proof state:
case pos.h₁
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ⊤
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
⊢ ↑C ≤ ‖f x‖ₑ

Tactic:
rwa [coe_le_enorm]

Result:
no goals