Bounded augmented reference map

The reference map is scaled pointwise by an invariant positive factor derived from its coordinate ℓ¹ size. This avoids choosing maxima while still placing every coordinate strictly inside (-1/2, 1/2). Adding the signed-interval coordinate then gives strict endpoint orthant signs.

noncomputable def NRR.PrimeConfigurationModel.referenceL1 {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : ℝ

Coordinate ℓ¹ size of the reference vector.

Equations

• M.referenceL1 x = ∑ i : Fin p, |↑(M.reference x) i|

theorem NRR.PrimeConfigurationModel.referenceL1_nonneg {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : 0 ≤ M.referenceL1 x

theorem NRR.PrimeConfigurationModel.continuous_referenceL1 {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : Continuous M.referenceL1

theorem NRR.PrimeConfigurationModel.referenceL1_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) : M.referenceL1 (g • x) = M.referenceL1 x

noncomputable def NRR.PrimeConfigurationModel.referenceScale {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : ℝ

Positive invariant scale used to bound every reference coordinate.

Equations

• M.referenceScale x = 1 / (2 * (1 + M.referenceL1 x))

theorem NRR.PrimeConfigurationModel.referenceScale_pos {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : 0 < M.referenceScale x

theorem NRR.PrimeConfigurationModel.continuous_referenceScale {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : Continuous M.referenceScale

theorem NRR.PrimeConfigurationModel.referenceScale_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) : M.referenceScale (g • x) = M.referenceScale x

theorem NRR.PrimeConfigurationModel.abs_reference_le_l1 {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) (i : Fin p) : |↑(M.reference x) i| ≤ M.referenceL1 x

noncomputable def NRR.PrimeConfigurationModel.scaledReference {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : C(M.Point, ZeroSum p)

The scaled reference vector.

Equations

• M.scaledReference = { toFun := fun (x : M.Point) => ⟨fun (i : Fin p) => M.referenceScale x * ↑(M.reference x) i, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem NRR.PrimeConfigurationModel.scaledReference_apply {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) (i : Fin p) : ↑(M.scaledReference x) i = M.referenceScale x * ↑(M.reference x) i

theorem NRR.PrimeConfigurationModel.scaledReference_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) : M.scaledReference (g • x) = g • M.scaledReference x

theorem NRR.PrimeConfigurationModel.abs_scaledReference_lt_half {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) (i : Fin p) : |↑(M.scaledReference x) i| < 1 / 2

def NRR.PrimeConfigurationModel.smulPointInterval {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (z : M.Point × ↑SignedInterval) : M.Point × ↑SignedInterval

Action on a model point and signed-interval coordinate.

Equations

• M.smulPointInterval g z = (g • z.1, z.2)

noncomputable def NRR.PrimeConfigurationModel.augmentedReference {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : M.Point × ↑SignedInterval → Fin p → ℝ

Reference vector augmented by the interval coordinate in the diagonal direction.

Equations

• M.augmentedReference z i = ↑(M.scaledReference z.1) i + ↑z.2

theorem NRR.PrimeConfigurationModel.continuous_augmentedReference {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : Continuous M.augmentedReference

theorem NRR.PrimeConfigurationModel.augmentedReference_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (z : M.Point × ↑SignedInterval) : M.augmentedReference (M.smulPointInterval g z) = g • M.augmentedReference z

theorem NRR.PrimeConfigurationModel.coordinateMean_augmentedReference {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (z : M.Point × ↑SignedInterval) : (coordinateMean p) (M.augmentedReference z) = ↑z.2

theorem NRR.PrimeConfigurationModel.coordinateDeviation_augmentedReference {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (z : M.Point × ↑SignedInterval) : (coordinateDeviation ⋯) (M.augmentedReference z) = M.scaledReference z.1

theorem NRR.PrimeConfigurationModel.scaledReference_eq_zero_iff {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : M.scaledReference x = 0 ↔ M.reference x = 0

theorem NRR.PrimeConfigurationModel.augmentedReference_eq_zero_iff {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (z : M.Point × ↑SignedInterval) : M.augmentedReference z = 0 ↔ M.reference z.1 = 0 ∧ z.2 = SignedInterval.center

theorem NRR.PrimeConfigurationModel.augmentedReference_left_mem_negative {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : M.augmentedReference (x, SignedInterval.left) ∈ negativeOrthant p

theorem NRR.PrimeConfigurationModel.augmentedReference_right_mem_positive {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : M.augmentedReference (x, SignedInterval.right) ∈ positiveOrthant p