-- Mathlib/Probability/IdentDistrib.lean
theorem eLpNorm_eq [NormedAddCommGroup γ] [OpensMeasurableSpace γ] (h : IdentDistrib f g μ ν)
    (p : ℝ≥0∞) : eLpNorm f p μ = eLpNorm g p ν

Proof state:
case neg.e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ IdentDistrib (fun x => ‖f x‖ₑ ^ p.toReal) (fun x => ‖g x‖ₑ ^ p.toReal) μ ν

Tactic:
exact h.comp (Measurable.pow_const (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)
  p.toReal)

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹

Tactic:
congr 1

Result:
case neg.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp only [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', one_div]

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν) ^ p.toReal⁻¹

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p μ = eLpNorm g p ν

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p μ = eLpNorm g p ν

Proof state:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ IdentDistrib (fun x => ‖f x‖ₑ) (fun x => ‖g x‖ₑ) μ ν

Tactic:
exact h.comp (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : β), ‖g a‖ₑ ^ p.toReal ∂ν

Tactic:
apply lintegral_eq

Result:
case neg.e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ IdentDistrib (fun x => ‖f x‖ₑ ^ p.toReal) (fun x => ‖g x‖ₑ ^ p.toReal) μ ν

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p μ = eLpNorm g p ν

Tactic:
simp only [h_top, eLpNorm, eLpNormEssSup, ENNReal.top_ne_zero, eq_self_iff_true, if_true,
  if_false]

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ essSup (fun x => ‖f x‖ₑ) μ = essSup (fun x => ‖g x‖ₑ) ν

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ essSup (fun x => ‖f x‖ₑ) μ = essSup (fun x => ‖g x‖ₑ) ν

Tactic:
apply essSup_eq

Result:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g μ ν
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ IdentDistrib (fun x => ‖f x‖ₑ) (fun x => ‖g x‖ₑ) μ ν