Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.cLpNorm_pow

APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:294 to 303

Mathematical statement

Exact Lean statement

lemma cLpNorm_pow (hp : p ≠ 0) {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) :
    ‖f ^ q‖ₙ_[p] = ‖f‖ₙ_[p * q] ^ q

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cLpNorm_pow (hp : p ≠ 0) {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) :    ‖f ^ q‖ₙ_[p] = ‖f‖ₙ_[p * q] ^ q := by  cases nonempty_fintype α  refine rpow_left_injOn (NNReal.coe_ne_zero.2 hp) (by dsimp; positivity)    (by dsimp; positivity) ?_  dsimp  rw [← rpow_natCast_mul (by positivity), ← mul_comm, ← ENNReal.coe_natCast, ← ENNReal.coe_mul,    ← NNReal.coe_natCast, ← NNReal.coe_mul, cLpNorm_rpow_eq_expect_norm hp,    cLpNorm_rpow_eq_expect_norm (by positivity)]  simp [← rpow_natCast_mul]