nnLpNorm

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -440,7 +440,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
         = (F ∗ μ C) x := by simp [sub_conv, F]
       _ = ∑ y, F y * μ C (x - y) := conv_eq_sum_sub' ..
       _ = ∑ y, F y * μ (x +ᵥ -C) y := by simp [neg_add_eq_sub]
-  rw [linftyNorm_eq_ciSup]
+  rw [linftyNorm_eq_iSup]
   refine ciSup_le fun x ↦ ?_
   calc
     ‖(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x‖

LeanAPAP/Prereqs/Convolution/Norm.lean

@@ -19,11 +19,11 @@ variable [RCLike β]
 
 @[simp] lemma lpNorm_trivChar (p : ℝ≥0∞) : ‖(trivChar : α → β)‖_[p] = 1 := by
   obtain _ | p := p
-  · simp only [ENNReal.none_eq_top, linftyNorm_eq_ciSup, trivChar_apply, apply_ite, norm_one,
+  · simp only [ENNReal.none_eq_top, linftyNorm_eq_iSup, trivChar_apply, apply_ite, norm_one,
       norm_zero]
     exact IsLUB.ciSup_eq ⟨by aesop (add simp mem_upperBounds), fun x hx ↦ hx ⟨0, if_pos rfl⟩⟩
   obtain rfl | hp := eq_or_ne p 0
-  · simp [l0Norm_eq_card]
+  · simp [l0Norm_eq_zero]
   · simp [lpNorm_eq_sum hp, apply_ite, hp]
 
 lemma conv_eq_inner (f g : α → β) (a : α) : (f ∗ g) a = ⟪conj f, τ a fun x ↦ g (-x)⟫_[β] := by

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -49,11 +49,11 @@ lemma nl2Norm_eq_expect (f : ∀ i, α i) : ‖f‖ₙ_[2] = sqrt (𝔼 i, ‖f
 
 lemma nl1Norm_eq_expect (f : ∀ i, α i) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [nlpNorm_eq_expect']
 
-lemma nl0Norm_eq_card (f : ∀ i, α i) : ‖f‖ₙ_[0] = {i | f i ≠ 0}.toFinite.toFinset.card := by
-  simp [l0Norm_eq_card, nlpNorm]
+lemma nl0Norm_eq_zero (f : ∀ i, α i) : ‖f‖ₙ_[0] = {i | f i ≠ 0}.toFinite.toFinset.card := by
+  simp [l0Norm_eq_zero, nlpNorm]
 
-lemma nlinftyNorm_eq_ciSup (f : ∀ i, α i) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by
-  simp [nlpNorm, linftyNorm_eq_ciSup]
+lemma nlinftyNorm_eq_iSup (f : ∀ i, α i) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by
+  simp [nlpNorm, linftyNorm_eq_iSup]
 
 @[simp] lemma nlpNorm_zero : ‖(0 : ∀ i, α i)‖ₙ_[p] = 0 := by simp [nlpNorm]
 
@@ -72,10 +72,10 @@ lemma nlpNorm_sub_comm (f g : ∀ i, α i) : ‖f - g‖ₙ_[p] = ‖g - f‖ₙ
 
 @[simp] lemma nlpNorm_eq_zero [Nonempty ι] : ‖f‖ₙ_[p] = 0 ↔ f = 0 := by
   obtain p | p := p
-  · simp [nlinftyNorm_eq_ciSup, ENNReal.none_eq_top, ←sup'_univ_eq_ciSup, le_antisymm_iff,
+  · simp [nlinftyNorm_eq_iSup, ENNReal.none_eq_top, ←sup'_univ_eq_ciSup, le_antisymm_iff,
       Function.funext_iff]
   obtain rfl | hp := eq_or_ne p 0
-  · simp [nl0Norm_eq_card, eq_empty_iff_forall_not_mem, Function.funext_iff]
+  · simp [nl0Norm_eq_zero, eq_empty_iff_forall_not_mem, Function.funext_iff]
   · rw [←rpow_eq_zero nlpNorm_nonneg (NNReal.coe_ne_zero.2 hp)]
     simp [nlpNorm_rpow_eq_expect hp, Fintype.expect_eq_zero_iff_of_nonneg, rpow_nonneg,
       Function.funext_iff, rpow_eq_zero _ (NNReal.coe_ne_zero.2 hp), Pi.le_def]
@@ -135,7 +135,7 @@ variable {α : Type*} [NormedAddCommGroup α] {p : ℝ≥0∞}
 @[simp]
 lemma nlpNorm_const [Nonempty ι] (hp : p ≠ 0) (a : α) : ‖const ι a‖ₙ_[p] = ‖a‖ := by
   obtain _ | p := p
-  · simp [nlinftyNorm_eq_ciSup]
+  · simp [nlinftyNorm_eq_iSup]
   have : (card ι : ℝ) ^ (p : ℝ)⁻¹ ≠ 0 := by positivity
   simp [nlpNorm, ENNReal.coe_ne_coe.1 hp, mul_div_cancel_left₀ _ this]
 

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -39,10 +39,10 @@ variable {α β : Type*} [AddCommGroup α] [Fintype α] {p : ℝ≥0∞}
 @[simp]
 lemma lpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ a f‖_[p] = ‖f‖_[p] := by
   obtain p | p := p
-  · simp only [linftyNorm_eq_ciSup, ENNReal.none_eq_top, translate_apply]
+  · simp only [linftyNorm_eq_iSup, ENNReal.none_eq_top, translate_apply]
     exact (Equiv.subRight _).iSup_congr fun _ ↦ rfl
   obtain rfl | hp := eq_or_ne p 0
-  · simp only [l0Norm_eq_card, translate_apply, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero,
+  · simp only [l0Norm_eq_zero, translate_apply, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero,
       Nat.cast_inj]
     exact card_equiv (Equiv.subRight a) (by simp)
   · simp only [lpNorm_eq_sum hp, ENNReal.some_eq_coe, translate_apply]
@@ -52,10 +52,10 @@ lemma lpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ
 @[simp] lemma lpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖_[p] = ‖f‖_[p] := by
   simp only [conjneg, lpNorm_conj]
   obtain p | p := p
-  · simp only [linftyNorm_eq_ciSup, ENNReal.none_eq_top, conjneg, RCLike.norm_conj]
+  · simp only [linftyNorm_eq_iSup, ENNReal.none_eq_top, conjneg, RCLike.norm_conj]
     exact (Equiv.neg _).iSup_congr fun _ ↦ rfl
   obtain rfl | hp := eq_or_ne p 0
-  · simp only [l0Norm_eq_card, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, Nat.cast_inj]
+  · simp only [l0Norm_eq_zero, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, Nat.cast_inj]
     exact card_equiv (Equiv.neg _) (by simp)
   · simp only [lpNorm_eq_sum hp, ENNReal.some_eq_coe]
     congr 1