Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.dLpNorm_translate

APAP.Prereqs.LpNorm.Discrete.Basic · APAP/Prereqs/LpNorm/Discrete/Basic.lean:88 to 98

Mathematical statement

Exact Lean statement

@[simp]
lemma dLpNorm_translate [NormedAddCommGroup E] (a : G) (f : G → E) : ‖τ a f‖_[p] = ‖f‖_[p]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]lemma dLpNorm_translate [NormedAddCommGroup E] (a : G) (f : G → E) : ‖τ a f‖_[p] = ‖f‖_[p] := by  cases nonempty_fintype G  obtain p | p := p  · simp only [dLinftyNorm_eq_iSup_norm, ENNReal.none_eq_top, translate_apply]    exact (Equiv.subRight _).iSup_congr fun _ ↦ rfl  obtain rfl | hp := eq_or_ne p 0  · simp only [dLpNorm_exponent_zero, ENNReal.some_eq_coe, ENNReal.coe_zero]  · simp only [dLpNorm_eq_sum_norm hp, ENNReal.some_eq_coe, translate_apply]    congr 1    exact Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl