Codimension calculation in ap_in_ff

LeanAPAP.lean

@@ -3,29 +3,35 @@ import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Group.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
 import LeanAPAP.Mathlib.Algebra.Order.Floor
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
+import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
+import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
+import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.Order.CompleteLattice
 import LeanAPAP.Mathlib.Order.Filter.Basic
+import LeanAPAP.Mathlib.Order.Hom.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
@@ -60,6 +66,7 @@ import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Inner.Compact
 import LeanAPAP.Prereqs.Inner.Discrete.Basic
 import LeanAPAP.Prereqs.Inner.Discrete.Defs
+import LeanAPAP.Prereqs.Inner.Function
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic

LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -0,0 +1,3 @@
+import Mathlib.Algebra.Group.Subgroup.Basic
+
+attribute [simp] AddMonoidHom.mem_ker

LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -1,5 +1,13 @@
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled
+
 /-!
 # TODO
 
 Rename `one_le_mul_of_one_le_of_one_le` to `one_le_mul₀`
 -/
+
+variable {G₀ : Type*} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀]
+  {a b : G₀} [PosMulMono G₀]
+
+-- TODO: Unify with `le_inv`
+lemma le_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := sorry

LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean

@@ -0,0 +1,4 @@
+import Mathlib.Algebra.Order.Ring.Cast
+
+@[gcongr] protected alias ⟨_, GCongr.intCast_mono⟩ := Int.cast_le
+@[gcongr] protected alias ⟨_, GCongr.intCast_strictMono⟩ := Int.cast_lt

LeanAPAP/Mathlib/Data/ENNReal/Basic.lean

@@ -0,0 +1,32 @@
+import Mathlib.Data.ENNReal.Basic
+
+namespace ENNReal
+
+@[simp] lemma ofNat_pos {n : ℕ} [n.AtLeastTwo] : 0 < (no_index OfNat.ofNat n : ℝ≥0∞) :=
+  Nat.cast_pos.2 Fin.size_pos'
+
+end ENNReal
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq Function ENNReal
+
+private lemma ennreal_one_pos : (0 : ℝ≥0∞) < 1 := zero_lt_one
+
+/-- The `positivity` extension which identifies expressions of the form `‖f‖_[p]`. -/
+@[positivity OfNat.ofNat _] def evalOfNatENNReal : PositivityExt where eval {u} α _z _p e := do
+  match u, α, e with
+  | 0, ~q(ℝ≥0∞), ~q(@OfNat.ofNat _ $n $instn) =>
+    try
+      let instn ← synthInstanceQ q(Nat.AtLeastTwo $n)
+      return Strictness.positive (q(@ofNat_pos $n $instn) : Expr)
+    catch _ => do
+      match n with
+      | ~q(1) => return .positive (q(ennreal_one_pos) : Expr)
+      | _ => throwError "not positive"
+  | _ => throwError "not `ENNReal`-valued `ofNat`"
+
+end Mathlib.Meta.Positivity
+
+open scoped ENNReal
+
+example : (0 : ℝ≥0∞) < 1 := by positivity

LeanAPAP/Mathlib/Data/ZMod/Module.lean

@@ -0,0 +1,8 @@
+import Mathlib.Data.ZMod.Module
+
+namespace AddSubgroup
+variable {n : ℕ} {M : Type*} [AddCommGroup M] [Module (ZMod n) M] {S : AddSubgroup M} {x : M}
+
+@[simp] lemma mem_toZModSubmodule : x ∈ toZModSubmodule n S ↔ x ∈ S := .rfl
+
+end AddSubgroup

LeanAPAP/Mathlib/Order/CompleteLattice.lean

@@ -0,0 +1,6 @@
+import Mathlib.Order.CompleteLattice
+
+variable {α : Type*} [CompleteLattice α]
+
+lemma iSup_le_iSup_of_imp {p q : Prop} {a : α} (h : p → q) : ⨆ _h : p, a ≤ ⨆ _h : q, a := by aesop
+lemma iInf_le_iInf_of_imp {p q : Prop} {a : α} (h : p → q) : ⨅ _h : q, a ≤ ⨅ _h : p, a := by aesop

LeanAPAP/Mathlib/Order/Hom/Basic.lean

@@ -0,0 +1,3 @@
+import Mathlib.Order.Hom.Basic
+
+@[gcongr] protected alias ⟨_, GCongr.orderIso_apply_le_apply⟩ := OrderIso.le_iff_le

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -348,7 +348,7 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m 
       gcongr; exact dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub (mod_cast hp)
     _ ≤ k * ε * ‖f‖_[2 * m] + k * ε * ‖f‖_[2 * m] := by push_cast; gcongr
 
-lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊)
+lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊)
     (h₁ : Lc * Sc ≤ ASc ^ k * Tc) (h₂ : (Ac : ℝ) ^ k / 2 ≤ Lc) (h₃ : (ASc : ℝ) ≤ K * Ac)
     (hAc : 0 < Ac) (hε : 0 < ε) (hε' : ε ≤ 1) (hm : 1 ≤ m) :
     K ^ (-512 * m / ε ^ 2 : ℝ) * Sc ≤ Tc := by
@@ -361,7 +361,7 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) *
   refine le_of_mul_le_mul_left ?_ this
   have : (Ac : ℝ) ^ k ≤ K * Lc := by
     rw [div_le_iff₀'] at h₂
-    refine h₂.trans (mul_le_mul_of_nonneg_right hK' (Nat.cast_nonneg _))
+    refine h₂.trans (mul_le_mul_of_nonneg_right hK₂ (Nat.cast_nonneg _))
     exact zero_lt_two
   rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm,
     inv_mul_le_iff (Real.rpow_pos_of_pos hK _)]
@@ -375,7 +375,7 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) *
   rw [mul_pow, ← mul_assoc, ← pow_succ']
   refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (Nat.cast_nonneg _) _)
   rw [← Real.rpow_natCast]
-  refine Real.rpow_le_rpow_of_exponent_le (one_le_two.trans hK') ?_
+  refine Real.rpow_le_rpow_of_exponent_le (one_le_two.trans hK₂) ?_
   rw [Nat.cast_add_one, ← le_sub_iff_add_le, hk']
   refine (Nat.ceil_lt_add_one ?_).le.trans ?_
   · positivity
@@ -391,7 +391,7 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) *
 
 -- trivially true for other reasons for big ε
 lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ)
-    (hK' : 2 ≤ K) (hK : σ[A, S] ≤ K) :
+    (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) :
     ∃ T : Finset G,
       K ^ (-512 * m / ε ^ 2 : ℝ) * S.card ≤ T.card ∧
         ∀ t ∈ T, ‖τ t (mu A ∗ f) - mu A ∗ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by
@@ -400,7 +400,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
   obtain rfl | hA := A.eq_empty_or_nonempty
   · refine ⟨univ, ?_, fun t _ ↦ ?_⟩
     · have : K ^ ((-512 : ℝ) * m / ε ^ 2) ≤ 1 := by
-        refine Real.rpow_le_one_of_one_le_of_nonpos (one_le_two.trans hK') ?_
+        refine Real.rpow_le_one_of_one_le_of_nonpos (one_le_two.trans hK₂) ?_
         rw [neg_mul, neg_div, Right.neg_nonpos_iff]
         positivity
       refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_
@@ -418,7 +418,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
   obtain ⟨a, ha, hL'⟩ := big_shifts S _ hk hL (filter_subset _ _)
   refine ⟨univ.filter fun t : G ↦ (a + fun _ ↦ -t) ∈ L, ?_, ?_⟩
   · simp_rw [sub_eq_add_neg] at hL'
-    exact T_bound hK' L.card S.card A.card (A + S).card _ rfl hL' this
+    exact T_bound hK₂ L.card S.card A.card (A + S).card _ rfl hL' this
       (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm
   intro t ht
   simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and_iff] at ht

LeanAPAP/Prereqs/Chang.lean

@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
+import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin
@@ -77,16 +78,9 @@ lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G}
 
 local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 
-variable [MeasurableSpace G]
+variable [MeasurableSpace G] [DiscreteMeasurableSpace G]
 
-private noncomputable def α (f : G → ℂ) := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
-
-lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity
-lemma α_pos (hf : f ≠ 0) : 0 < α f := by unfold α; sorry -- positivity
-
-variable [DiscreteMeasurableSpace G]
-
-lemma α_le_one (f : G → ℂ) : α f ≤ 1 := by
+private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G ≤ 1 := by
   refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_
   any_goals positivity
   rw [dL1Norm_eq_sum_nnnorm, dL2Norm_sq_eq_sum_nnnorm, ← NNReal.coe_le_coe]
@@ -159,44 +153,47 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
       mul_left_comm (Algebra.cast (ν _ : ℝ) : ℂ), ← mul_sum, ← sub_eq_add_neg, sum_sub_distrib,
       Complex.conj_ofReal, mul_comm (Algebra.cast (ν _ : ℝ) : ℂ)]
     rfl
-  sorry
-  sorry
-  -- positivity
+  positivity
+
+open scoped ComplexOrder
 
 lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) :
-    ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * α f) ≤ boringEnergy m Δ := by
+    Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)) ≤ boringEnergy m Δ := by
   have hG : (0 : ℝ) < card G := by positivity
-  simpa [boringEnergy, α, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc,
+  simpa [boringEnergy, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc,
     div_le_iff₀ hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using
     general_hoelder hη 1 (fun (_ : G) _ ↦ le_rfl) hΔ hm
 
 /-- **Chang's lemma**. -/
 lemma chang (hf : f ≠ 0) (hη : 0 < η) :
     ∃ Δ, Δ ⊆ largeSpec f η ∧
-      Δ.card ≤ ⌈changConst * exp 1 * ⌈𝓛 (α f)⌉₊ / η ^ 2⌉₊ ∧ largeSpec f η ⊆ Δ.addSpan := by
+      Δ.card ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
+      largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
   obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ Δ.card
   · simp [hΔ']
-  have : 0 < α f := α_pos hf
-  set β := ⌈𝓛 (α f)⌉₊
+  let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
+  have : 0 < α := by positivity
+  set β := ⌈𝓛 α⌉₊
   have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) $ α_le_one _)
+  have : 0 < ‖f‖_[1] := by positivity
   refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
-    (by positivity : 0 < ↑Δ.card ^ β * (η ^ (2 * β) * α f))
+    (by positivity : 0 < Δ.card ^ β * (η ^ (2 * β) * α))
   push_cast
   rw [← mul_assoc, ← pow_add, ← two_mul]
   refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_
   refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_
   rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ← pow_mul, mul_div_assoc]
   calc
     _ = (changConst * Δ.card * β) ^ β := by ring
-    _ ≤ (changConst * Δ.card * β) ^ β * (α f * exp β) := ?_
-    _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α f * exp β) := by
-        rw [div_self hη.ne', one_pow, one_mul]
+    _ ≤ (changConst * Δ.card * β) ^ β * (α * exp β) := ?_
+    _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by
+      rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
   refine le_mul_of_one_le_right (by positivity) ?_
   rw [← inv_pos_le_iff_one_le_mul']
   calc
-    (α f)⁻¹ = exp (0 + log (α f)⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
-    _ ≤ exp ⌈0 + log (α f)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
+    α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
+    _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
     _ ≤ exp β := by unfold_let β; gcongr; exact zero_le_one
   all_goals positivity

LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean

@@ -116,6 +116,9 @@ lemma conv_right_comm (f g h : G → R) : f ∗ g ∗ h = f ∗ h ∗ g := by
 lemma conv_left_comm (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (f ∗ h) := by
   rw [← conv_assoc, ← conv_assoc, conv_comm g]
 
+lemma conv_rotate (f g h : G → R) : f ∗ g ∗ h = g ∗ h ∗ f := by rw [conv_assoc, conv_comm]
+lemma conv_rotate' (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (h ∗ f) := by rw [conv_comm, ← conv_assoc]
+
 lemma conv_conv_conv_comm (f g h i : G → R) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i) := by
   rw [conv_assoc, conv_assoc, conv_left_comm g]
 

LeanAPAP/Prereqs/Function/Indicator/Defs.lean

@@ -108,11 +108,10 @@ lemma indicate_inf [Fintype α] (s : Finset ι) (t : ι → Finset α) :
 
 variable [StarRing β]
 
-@[simp] lemma conj_indicate_apply [AddCommGroup α] (s : Finset α) (a : α) :
-    conj (𝟭_[β] s a) = 𝟭 s a := by simp [indicate_apply]
+@[simp] lemma conj_indicate_apply (s : Finset α) (a : α) : conj (𝟭_[β] s a) = 𝟭 s a := by
+  simp [indicate_apply]
 
-@[simp] lemma conj_indicate [AddCommGroup α] (s : Finset α) : conj (𝟭_[β] s) = 𝟭 s := by
-  ext; simp
+@[simp] lemma conj_indicate (s : Finset α) : conj (𝟭_[β] s) = 𝟭 s := by ext; simp
 
 end CommSemiring
 
@@ -224,7 +223,7 @@ end Group
 end DivisionSemiring
 
 section Semifield
-variable (β) [Semifield β] [StarRing β] [AddCommGroup α] {s : Finset α}
+variable (β) [Semifield β] [StarRing β] {s : Finset α}
 
 @[simp] lemma conj_mu_apply (s : Finset α) (a : α) : conj (μ_[β] s a) = μ s a := by simp [mu]
 

LeanAPAP/Prereqs/Inner/Function.lean

@@ -0,0 +1,30 @@
+import LeanAPAP.Prereqs.Expect.Basic
+import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
+
+open Finset MeasureTheory
+open scoped BigOperators ComplexConjugate
+
+variable {α R : Type*} [Fintype α] [DecidableEq α]
+
+section CommSemiring
+variable [CommSemiring R] [StarRing R]
+
+lemma indicate_dL2Inner (s : Finset α) (f : α → R) : ⟪𝟭 s, f⟫_[R] = ∑ i ∈ s, f i := by
+  simp [dL2Inner, indicate_apply]
+
+lemma dL2Inner_indicate (f : α → R) (s : Finset α) : ⟪f, 𝟭 s⟫_[R] = ∑ i ∈ s, conj (f i) := by
+  simp [dL2Inner, indicate_apply]
+
+end CommSemiring
+
+section Semifield
+variable [Semifield R] [CharZero R] [StarRing R]
+
+lemma mu_dL2Inner (s : Finset α) (f : α → R) : ⟪μ s, f⟫_[R] = 𝔼 i ∈ s, f i := by
+  simp [dL2Inner, indicate_apply]; simp [mu_apply, expect_eq_sum_div_card, mul_sum, div_eq_inv_mul]
+
+lemma dL2Inner_mu (f : α → R) (s : Finset α) : ⟪f, μ s⟫_[R] = 𝔼 i ∈ s, conj (f i) := by
+  simp [dL2Inner, indicate_apply]; simp [mu_apply, expect_eq_sum_div_card, sum_mul, div_eq_mul_inv]
+
+end Semifield

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -55,6 +55,10 @@ lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1
 
 lemma dL1Norm_mu_le_one : ‖μ_[R] s‖_[1] ≤ 1 := by simpa using dLpNorm_mu_le le_rfl
 
+@[simp] lemma dL2Norm_mu (hs : s.Nonempty) : ‖μ_[R] s‖_[2] = s.card ^ (-2⁻¹ : ℝ) := by
+  have : (2⁻¹ - 1 : ℝ) = -2⁻¹ := by norm_num
+  simpa [sqrt_eq_rpow, this] using dLpNorm_mu one_le_two (R := R) hs
+
 end Indicator
 
 /-! ### Translation -/