Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.cLpNorm_translate

APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:386 to 396

Mathematical statement

Exact Lean statement

@[simp]
lemma cLpNorm_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 cLpNorm_translate [NormedAddCommGroup E] (a : G) (f : G → E) : ‖τ a f‖ₙ_[p] = ‖f‖ₙ_[p] := by  cases nonempty_fintype G  obtain p | p := p  · simp only [cLpNorm_exponent_top_eq_essSup, ENNReal.none_eq_top, translate_apply]    exact (Equiv.subRight _).iSup_congr fun _ ↦ rfl  obtain rfl | hp := eq_or_ne p 0  · simp only [cLpNorm_exponent_zero, ENNReal.some_eq_coe, ENNReal.coe_zero]  · simp only [cLpNorm_eq_expect_norm hp, ENNReal.some_eq_coe, translate_apply]    congr 1    exact Fintype.expect_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl