-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_restrict_eq_of_support_subset {s : Set α} {f : α → F} (hsf : f.support ⊆ s) :
    eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ‖f x‖ₑ) (μ.restrict s) = essSup (fun x => ‖f x‖ₑ) μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ¬p.toReal ≤ 0

Tactic:
simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top, eLpNorm'_eq_lintegral_enorm]

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Proof state:
case neg.e_a.hsf
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (Function.support fun x => ‖f x‖ₑ ^ p.toReal) ⊆ s

Tactic:
have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top

Result:
case neg.e_a.hsf
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
this : ¬p.toReal ≤ 0
⊢ (Function.support fun x => ‖f x‖ₑ ^ p.toReal) ⊆ s

Proof state:
case neg.e_a
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Tactic:
apply setLIntegral_eq_of_support_subset

Result:
case neg.e_a.hsf
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (Function.support fun x => ‖f x‖ₑ ^ p.toReal) ⊆ s

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp [hp0]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
congr 1

Result:
case neg.e_a
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Proof state:
case neg.e_a.hsf
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ⊤
this : ¬p.toReal ≤ 0
⊢ (Function.support fun x => ‖f x‖ₑ ^ p.toReal) ⊆ s

Tactic:
simpa [this] using hsf

Result:
no goals

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
f : α → F
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ‖f x‖ₑ) (μ.restrict s) = essSup (fun x => ‖f x‖ₑ) μ

Tactic:
exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx

Result:
no goals