-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_map_measure (hg : AEStronglyMeasurable g (Measure.map f μ))
    (hf : AEMeasurable f μ) : eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [lintegral_map' (hg.enorm.pow_const p.toReal) hf]

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top]

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [hp_top, eLpNorm_exponent_top]

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ⊤
⊢ eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
exact eLpNormEssSup_map_measure hg hf

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ