Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.dLpNorm_pow

APAP.Prereqs.LpNorm.Discrete.Defs · APAP/Prereqs/LpNorm/Discrete/Defs.lean:289 to 298

Mathematical statement

Exact Lean statement

lemma dLpNorm_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 dLpNorm_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, dLpNorm_rpow_eq_sum_norm hp,    dLpNorm_rpow_eq_sum_norm (by positivity)]  simp [← rpow_natCast_mul]