Foundations for binary and spherical code bounds

Elementary coding-theory definitions, projection certificates, and the finite Johnson bound.

instance MetricCodes.numeralTwoAtLeast : Nat.AtLeastTwo 2

@[reducible, inline]

abbrev MetricCodes.Ambient (n : ℕ) : Type

The ambient used in the metric-code argument.

Equations

• MetricCodes.Ambient n = EuclideanSpace ℝ (Fin n)

@[reducible, inline]

abbrev MetricCodes.BinaryWord (n : ℕ) : Type

The binary word used in the metric-code argument.

Equations

• MetricCodes.BinaryWord n = (Fin n → Bool)

@[reducible, inline]

abbrev MetricCodes.hammingDist {n : ℕ} (x y : BinaryWord n) : ℕ

The hamming dist used in the metric-code argument.

Equations

• MetricCodes.hammingDist x y = hammingDist x y

theorem MetricCodes.hammingDist_self {n : ℕ} (x : BinaryWord n) : hammingDist x x = 0

def MetricCodes.binaryWeight {n : ℕ} (x : BinaryWord n) : ℕ

The binary weight used in the metric-code argument.

Equations

• MetricCodes.binaryWeight x = {i : Fin n | x i = true}.card

def MetricCodes.IsBinaryCode {n : ℕ} (d : ℕ) (C : Finset (BinaryWord n)) : Prop

The predicate asserting binary code.

Equations

• MetricCodes.IsBinaryCode d C = ∀ ⦃x : MetricCodes.BinaryWord n⦄, x ∈ C → ∀ ⦃y : MetricCodes.BinaryWord n⦄, y ∈ C → x ≠ y → d ≤ MetricCodes.hammingDist x y

@[reducible, inline]

abbrev MetricCodes.JohnsonSphere (n w : ℕ) : Type

The johnson sphere used in the Johnson-code argument.

Equations

• MetricCodes.JohnsonSphere n w = { x : MetricCodes.BinaryWord n // MetricCodes.binaryWeight x = w }

noncomputable def MetricCodes.hammingCorrelation {n : ℕ} (x y : BinaryWord n) : ℝ

The hamming correlation used in the metric-code argument.

Equations

• MetricCodes.hammingCorrelation x y = 1 - 2 * ↑(MetricCodes.hammingDist x y) / ↑n

@[simp]

theorem MetricCodes.hammingCorrelation_self {n : ℕ} (x : BinaryWord n) : hammingCorrelation x x = 1

theorem MetricCodes.hammingCorrelation_le_of_dist_le {n d : ℕ} (hn : 0 < n) {x y : BinaryWord n} (hd : d ≤ hammingDist x y) : hammingCorrelation x y ≤ 1 - 2 * ↑d / ↑n

noncomputable def MetricCodes.sphericalEntropy (u : ℝ) : ℝ

The spherical entropy used in the metric-code argument.

Equations

• MetricCodes.sphericalEntropy u = (1 + u) * Real.logb 2 (1 + u) - u * Real.logb 2 u

@[simp]

theorem MetricCodes.sphericalEntropy_zero : sphericalEntropy 0 = 0

theorem MetricCodes.sphericalEntropy_eq_log_add {u : ℝ} (hu : 0 < u) : sphericalEntropy u = Real.logb 2 (1 + u) + u * Real.logb 2 ((1 + u) / u)

noncomputable def MetricCodes.binaryEntropy (u : ℝ) : ℝ

The binary entropy used in the metric-code argument.

Equations

• MetricCodes.binaryEntropy u = -(u * Real.logb 2 u) - (1 - u) * Real.logb 2 (1 - u)

@[simp]

theorem MetricCodes.binaryEntropy_zero : binaryEntropy 0 = 0

theorem MetricCodes.binaryEntropy_nonneg {u : ℝ} (hu : 0 ≤ u) (hu' : u ≤ 1) : 0 ≤ binaryEntropy u

noncomputable def MetricCodes.Gamma (a b : ℝ) : ℝ

The gamma used in the metric-code argument.

Equations

• MetricCodes.Gamma a b = (a - b) * (1 + a + b) / ((1 + 2 * a) * √(a * (1 + a)))

theorem MetricCodes.Gamma_eq_sub (a b : ℝ) : Gamma a b = (a * (1 + a) - b * (1 + b)) / ((1 + 2 * a) * √(a * (1 + a)))

noncomputable def MetricCodes.classicalThreshold (s : ℝ) : ℝ

The classical threshold used in the metric-code argument.

Equations

• MetricCodes.classicalThreshold s = (1 / √(1 - s ^ 2) - 1) / 2

@[simp]

theorem MetricCodes.classicalThreshold_zero : classicalThreshold 0 = 0

theorem MetricCodes.classicalThreshold_pos {s : ℝ} (hs : 0 < s) (hs' : s < 1) : 0 < classicalThreshold s

def MetricCodes.booleanHarmonicDimension (n : ℕ) : ℕ → ℕ

The boolean harmonic dimension used in the metric-code argument.

Equations

• MetricCodes.booleanHarmonicDimension n 0 = 1
• MetricCodes.booleanHarmonicDimension n k.succ = n.choose (k + 1) - n.choose k

theorem MetricCodes.booleanHarmonicDimension_succ (n k : ℕ) : booleanHarmonicDimension n (k + 1) = n.choose (k + 1) - n.choose k

theorem MetricCodes.sum_booleanHarmonicDimension (n L : ℕ) (hL : 2 * L ≤ n) : ∑ k ∈ Finset.range (L + 1), booleanHarmonicDimension n k = n.choose L

@[reducible, inline]

abbrev MetricCodes.hammingFibreDimension (n k : ℕ) : ℕ

The hamming fibre dimension used in the metric-code argument.

Equations

• MetricCodes.hammingFibreDimension n k = MetricCodes.booleanHarmonicDimension n k

def MetricCodes.johnsonFibreDimension (n w p q : ℕ) : ℕ

The johnson fibre dimension used in the metric-code argument.

Equations

• MetricCodes.johnsonFibreDimension n w p q = MetricCodes.booleanHarmonicDimension w p * MetricCodes.booleanHarmonicDimension (n - w) q

noncomputable def MetricCodes.hammingJacobiEntry (n k i : ℕ) : ℝ

The hamming jacobi entry used in the metric-code argument.

Equations

• MetricCodes.hammingJacobiEntry n k i = (↑i - ↑k + 1) * (↑n - ↑i - ↑k) / (↑n * √((↑i + 1) * (↑n - ↑i)))

theorem MetricCodes.hammingJacobiEntry_pos {n k i : ℕ} (hn : 0 < n) (hki : k ≤ i) (hi : i + k < n) : 0 < hammingJacobiEntry n k i

noncomputable def MetricCodes.hammingJacobiMatrix (n k L : ℕ) : Matrix (Fin (L - k + 1)) (Fin (L - k + 1)) ℝ

The hamming jacobi matrix used in the metric-code argument.

Equations

• MetricCodes.hammingJacobiMatrix n k L p q = if ↑p + 1 = ↑q then MetricCodes.hammingJacobiEntry n k (k + ↑p) else if ↑q + 1 = ↑p then MetricCodes.hammingJacobiEntry n k (k + ↑q) else 0

theorem MetricCodes.hammingJacobiMatrix_symmetric (n k L : ℕ) : (hammingJacobiMatrix n k L).transpose = hammingJacobiMatrix n k L

noncomputable def MetricCodes.hammingGamma (a b : ℝ) : ℝ

The hamming gamma used in the metric-code argument.

Equations

• MetricCodes.hammingGamma a b = 2 * (a - b) * (1 - a - b) / √(a * (1 - a))

noncomputable def MetricCodes.johnsonJ1 (w p : ℕ) : ℝ

The johnson j1 used in the metric-code argument.

Equations

• MetricCodes.johnsonJ1 w p = ↑w / 2 - ↑p

noncomputable def MetricCodes.johnsonJ2 (n w q : ℕ) : ℝ

The johnson j2 used in the metric-code argument.

Equations

• MetricCodes.johnsonJ2 n w q = ↑(n - w) / 2 - ↑q

noncomputable def MetricCodes.johnsonJ (n j : ℕ) : ℝ

The johnson j used in the metric-code argument.

Equations

• MetricCodes.johnsonJ n j = ↑n / 2 - ↑j

noncomputable def MetricCodes.johnsonM (n w : ℕ) : ℝ

The johnson m used in the metric-code argument.

Equations

• MetricCodes.johnsonM n w = ↑n / 2 - ↑w

noncomputable def MetricCodes.johnsonSigma (n w p q : ℕ) : ℝ

The johnson sigma used in the metric-code argument.

Equations

• MetricCodes.johnsonSigma n w p q = MetricCodes.johnsonJ1 w p + MetricCodes.johnsonJ2 n w q

noncomputable def MetricCodes.johnsonDelta (n w p q : ℕ) : ℝ

The johnson delta used in the metric-code argument.

Equations

• MetricCodes.johnsonDelta n w p q = MetricCodes.johnsonJ2 n w q - MetricCodes.johnsonJ1 w p

def MetricCodes.johnsonLastDegree (n w p q : ℕ) : ℕ

The johnson last degree used in the metric-code argument.

Equations

• MetricCodes.johnsonLastDegree n w p q = min w (min (w - p + q) (n - w + p - q))

noncomputable def MetricCodes.johnsonMu (n w p q j : ℕ) : ℝ

The johnson mu used in the metric-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.johnsonNu (n w p q j : ℕ) : ℝ

The johnson nu used in the metric-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.johnsonDiagonal (n w p q j : ℕ) : ℝ

The johnson diagonal used in the metric-code argument.

Equations

• MetricCodes.johnsonDiagonal n w p q j = (↑n * MetricCodes.johnsonMu n w p q j - MetricCodes.johnsonM n w ^ 2) / (↑w * ↑(n - w))

noncomputable def MetricCodes.johnsonEdge (n w p q j : ℕ) : ℝ

The johnson edge used in the metric-code argument.

Equations

• MetricCodes.johnsonEdge n w p q j = ↑n * MetricCodes.johnsonNu n w p q j / (↑w * ↑(n - w))

noncomputable def MetricCodes.johnsonZonalDiagonal (n w j : ℕ) : ℝ

The johnson zonal diagonal used in the metric-code argument.

Equations

• MetricCodes.johnsonZonalDiagonal n w j = MetricCodes.johnsonDiagonal n w 0 0 j

noncomputable def MetricCodes.johnsonZonalEdge (n w j : ℕ) : ℝ

The johnson zonal edge used in the metric-code argument.

Equations

• MetricCodes.johnsonZonalEdge n w j = MetricCodes.johnsonEdge n w 0 0 j

noncomputable def MetricCodes.johnsonHattedDiagonal (n w p q j : ℕ) : ℝ

The johnson hatted diagonal used in the metric-code argument.

Equations

• MetricCodes.johnsonHattedDiagonal n w p q j = if j = 0 then 0 else MetricCodes.johnsonDiagonal n w p q j ^ 2 / MetricCodes.johnsonZonalDiagonal n w j

noncomputable def MetricCodes.johnsonHattedEdge (n w p q j : ℕ) : ℝ

The johnson hatted edge used in the metric-code argument.

Equations

• MetricCodes.johnsonHattedEdge n w p q j = MetricCodes.johnsonEdge n w p q j ^ 2 / MetricCodes.johnsonZonalEdge n w j

theorem MetricCodes.johnsonHattedDiagonal_nonneg {n w p q j : ℕ} (hzero : 0 < johnsonZonalDiagonal n w j) : 0 ≤ johnsonHattedDiagonal n w p q j

noncomputable def MetricCodes.johnsonJacobiMatrix (n w p q L : ℕ) : Matrix (Fin (L - (p + q) + 1)) (Fin (L - (p + q) + 1)) ℝ

The johnson jacobi matrix used in the metric-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.johnsonJacobiMatrix_diag (n w p q L : ℕ) (i : Fin (L - (p + q) + 1)) : johnsonJacobiMatrix n w p q L i i = johnsonHattedDiagonal n w p q (p + q + ↑i)

theorem MetricCodes.johnsonJacobiMatrix_symmetric (n w p q L : ℕ) : (johnsonJacobiMatrix n w p q L).transpose = johnsonJacobiMatrix n w p q L

@[reducible, inline]

abbrev MetricCodes.Boolean.Function (n : ℕ) : Type

The function used in the binary-code argument.

Equations

• MetricCodes.Boolean.Function n = (Finset (Fin n) → ℝ)

@[reducible, inline]

abbrev MetricCodes.Boolean.Level (n k : ℕ) : Type

The level used in the binary-code argument.

Equations

• MetricCodes.Boolean.Level n k = { S : Finset (Fin n) // S.card = k }

theorem MetricCodes.Boolean.card_level (n k : ℕ) : Fintype.card (Level n k) = n.choose k

def MetricCodes.Boolean.raiseAt {n : ℕ} (a : Fin n) (f : Function n) (S : Finset (Fin n)) : ℝ

The raise at used in the binary-code argument.

Equations

• MetricCodes.Boolean.raiseAt a f S = if a ∈ S then f (S.erase a) else 0

def MetricCodes.Boolean.lowerAt {n : ℕ} (a : Fin n) (f : Function n) (S : Finset (Fin n)) : ℝ

The lower at used in the binary-code argument.

Equations

• MetricCodes.Boolean.lowerAt a f S = if a ∈ S then 0 else f (insert a S)

def MetricCodes.Boolean.raise {n : ℕ} (f : Function n) (S : Finset (Fin n)) : ℝ

The raise used in the binary-code argument.

Equations

• MetricCodes.Boolean.raise f S = ∑ a : Fin n, MetricCodes.Boolean.raiseAt a f S

def MetricCodes.Boolean.lower {n : ℕ} (f : Function n) (S : Finset (Fin n)) : ℝ

The lower used in the binary-code argument.

Equations

• MetricCodes.Boolean.lower f S = ∑ a : Fin n, MetricCodes.Boolean.lowerAt a f S

def MetricCodes.Boolean.IsLevel {n : ℕ} (k : ℕ) (f : Function n) : Prop

The predicate asserting level.

Equations

• MetricCodes.Boolean.IsLevel k f = ∀ (S : Finset (Fin n)), S.card ≠ k → f S = 0

def MetricCodes.Boolean.IsHarmonic {n : ℕ} (k : ℕ) (f : Function n) : Prop

The predicate asserting harmonic.

Equations

• MetricCodes.Boolean.IsHarmonic k f = (MetricCodes.Boolean.IsLevel k f ∧ ∀ (S : Finset (Fin n)), MetricCodes.Boolean.lower f S = 0)

theorem MetricCodes.Boolean.lowerAt_raiseAt_of_ne {n : ℕ} (f : Function n) (a b : Fin n) (hab : a ≠ b) (S : Finset (Fin n)) : lowerAt a (raiseAt b f) S = raiseAt b (lowerAt a f) S

theorem MetricCodes.Boolean.lowerAt_raiseAt_self {n : ℕ} (f : Function n) (a : Fin n) (S : Finset (Fin n)) : lowerAt a (raiseAt a f) S = if a ∈ S then 0 else f S

theorem MetricCodes.Boolean.raiseAt_lowerAt_self {n : ℕ} (f : Function n) (a : Fin n) (S : Finset (Fin n)) : raiseAt a (lowerAt a f) S = if a ∈ S then f S else 0

theorem MetricCodes.Boolean.lowerAt_raise {n : ℕ} (f : Function n) (a : Fin n) (S : Finset (Fin n)) : lowerAt a (raise f) S = ∑ b : Fin n, lowerAt a (raiseAt b f) S

theorem MetricCodes.Boolean.raiseAt_lower {n : ℕ} (f : Function n) (a : Fin n) (S : Finset (Fin n)) : raiseAt a (lower f) S = ∑ b : Fin n, raiseAt a (lowerAt b f) S

theorem MetricCodes.Boolean.sum_mem_indicator {n : ℕ} (S : Finset (Fin n)) (x : ℝ) : (∑ a : Fin n, if a ∈ S then x else 0) = ↑S.card * x

theorem MetricCodes.Boolean.lower_raise_sub_raise_lower {n : ℕ} (f : Function n) (S : Finset (Fin n)) : lower (raise f) S - raise (lower f) S = (↑n - 2 * ↑S.card) * f S

theorem MetricCodes.Boolean.lower_raise_sub_raise_lower_of_level {n k : ℕ} (f : Function n) (hf : IsLevel k f) (S : Finset (Fin n)) : lower (raise f) S - raise (lower f) S = (↑n - 2 * ↑k) * f S

theorem MetricCodes.Boolean.lower_raise_of_harmonic {n k : ℕ} (f : Function n) (hf : IsHarmonic k f) (S : Finset (Fin n)) : lower (raise f) S = (↑n - 2 * ↑k) * f S

theorem MetricCodes.Boolean.raise_add {n : ℕ} (f g : Function n) : raise (f + g) = raise f + raise g

theorem MetricCodes.Boolean.raise_smul {n : ℕ} (c : ℝ) (f : Function n) : raise (c • f) = c • raise f

theorem MetricCodes.Boolean.lower_add {n : ℕ} (f g : Function n) : lower (f + g) = lower f + lower g

theorem MetricCodes.Boolean.lower_smul {n : ℕ} (c : ℝ) (f : Function n) : lower (c • f) = c • lower f

def MetricCodes.Boolean.raiseLinear (n : ℕ) : Function n →ₗ[ℝ] Function n

The raise linear used in the binary-code argument.

Equations

• MetricCodes.Boolean.raiseLinear n = { toFun := MetricCodes.Boolean.raise, map_add' := ⋯, map_smul' := ⋯ }

def MetricCodes.Boolean.lowerLinear (n : ℕ) : Function n →ₗ[ℝ] Function n

The lower linear used in the binary-code argument.

Equations

• MetricCodes.Boolean.lowerLinear n = { toFun := MetricCodes.Boolean.lower, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MetricCodes.Boolean.raiseLinear_apply {n : ℕ} (f : Function n) : (raiseLinear n) f = raise f

theorem MetricCodes.Boolean.IsLevel.raise {n k : ℕ} {f : Function n} (hf : IsLevel k f) : IsLevel (k + 1) (Boolean.raise f)

theorem MetricCodes.Boolean.IsLevel.lower {n k : ℕ} {f : Function n} (hf : IsLevel (k + 1) f) : IsLevel k (Boolean.lower f)

def MetricCodes.Boolean.raised {n : ℕ} (f : Function n) : ℕ → Function n

The raised used in the binary-code argument.

Equations

• MetricCodes.Boolean.raised f 0 = f
• MetricCodes.Boolean.raised f k.succ = MetricCodes.Boolean.raise (MetricCodes.Boolean.raised f k)

@[simp]

theorem MetricCodes.Boolean.raised_succ {n : ℕ} (f : Function n) (r : ℕ) : raised f (r + 1) = raise (raised f r)

theorem MetricCodes.Boolean.IsLevel.raised {n k : ℕ} {f : Function n} (hf : IsLevel k f) (r : ℕ) : IsLevel (k + r) (Boolean.raised f r)

def MetricCodes.Boolean.harmonicCoefficient (n k r : ℕ) : ℝ

The harmonic coefficient used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicCoefficient n k r = ↑r * (↑n - 2 * ↑k - ↑r + 1)

@[simp]

theorem MetricCodes.Boolean.harmonicCoefficient_zero (n k : ℕ) : harmonicCoefficient n k 0 = 0

theorem MetricCodes.Boolean.harmonicCoefficient_succ (n k r : ℕ) : harmonicCoefficient n k (r + 1) = harmonicCoefficient n k r + (↑n - 2 * ↑(k + r))

theorem MetricCodes.Boolean.lower_raised_succ_of_harmonic {n k : ℕ} (f : Function n) (hf : IsHarmonic k f) (r : ℕ) : lower (raised f (r + 1)) = harmonicCoefficient n k (r + 1) • raised f r

def MetricCodes.Boolean.toggle {n : ℕ} (a : Fin n) (S : Finset (Fin n)) : Finset (Fin n)

Toggle membership of the coordinate a in a finite subset.

Equations

• MetricCodes.Boolean.toggle a S = if a ∈ S then S.erase a else insert a S

@[simp]

theorem MetricCodes.Boolean.toggle_toggle {n : ℕ} (a : Fin n) (S : Finset (Fin n)) : toggle a (toggle a S) = S

def MetricCodes.Boolean.dot {n : ℕ} (f g : Function n) : ℝ

The dot used in the binary-code argument.

Equations

• MetricCodes.Boolean.dot f g = ∑ S : Finset (Fin n), f S * g S

theorem MetricCodes.Boolean.dot_raiseAt_eq_lowerAt {n : ℕ} (a : Fin n) (f g : Function n) : dot (raiseAt a f) g = dot f (lowerAt a g)

theorem MetricCodes.Boolean.dot_raise_eq_lower {n : ℕ} (f g : Function n) : dot (raise f) g = dot f (lower g)

theorem MetricCodes.Boolean.dot_comm {n : ℕ} (f g : Function n) : dot f g = dot g f

theorem MetricCodes.Boolean.dot_smul_right {n : ℕ} (f g : Function n) (c : ℝ) : dot f (c • g) = c * dot f g

theorem MetricCodes.Boolean.normSq_nonneg {n : ℕ} (f : Function n) : 0 ≤ dot f f

@[simp]

theorem MetricCodes.Boolean.normSq_eq_zero_iff {n : ℕ} (f : Function n) : dot f f = 0 ↔ f = 0

structure MetricCodes.ProjectionFamily (X : Type u_1) (D d : ℕ) : Type u_1

Data encoding the projection family construction.

• projection : X → Matrix (Fin D) (Fin D) ℝ

  The projection component.

• symmetric (x : X) : (self.projection x).transpose = self.projection x
• idempotent (x : X) : self.projection x * self.projection x = self.projection x
• trace_eq (x : X) : (self.projection x).trace = ↑d

def MetricCodes.ProjectionFamily.overlap {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (x y : X) : ℝ

The overlap used in the metric-code argument.

Equations

• P.overlap x y = (P.projection x * P.projection y).trace

@[simp]

theorem MetricCodes.ProjectionFamily.overlap_self {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (x : X) : P.overlap x x = ↑d

theorem MetricCodes.ProjectionFamily.overlap_eq_trace_sq {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (x y : X) : P.overlap x y = ((P.projection x * P.projection y).conjTranspose * (P.projection x * P.projection y)).trace

theorem MetricCodes.ProjectionFamily.overlap_nonneg {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (x y : X) : 0 ≤ P.overlap x y

theorem MetricCodes.ProjectionFamily.sq_trace_le_dimension_mul_trace_sq {D : ℕ} (A : Matrix (Fin D) (Fin D) ℝ) : A.trace ^ 2 ≤ ↑D * (A.transpose * A).trace

theorem MetricCodes.ProjectionFamily.sum_symmetric {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (C : Finset X) : (∑ x ∈ C, P.projection x).transpose = ∑ x ∈ C, P.projection x

theorem MetricCodes.ProjectionFamily.sum_overlap_eq_trace_mul_sum {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (C : Finset X) : ∑ x ∈ C, ∑ y ∈ C, P.overlap x y = ((∑ x ∈ C, P.projection x) * ∑ y ∈ C, P.projection y).trace

theorem MetricCodes.ProjectionFamily.card_mul_rank_sq_le_dimension_mul_sum_overlap {X : Type u_1} {D d : ℕ} (P : ProjectionFamily X D d) (C : Finset X) : (↑C.card * ↑d) ^ 2 ≤ ↑D * ∑ x ∈ C, ∑ y ∈ C, P.overlap x y

theorem MetricCodes.gram_double_sum_nonneg {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Finset X) (q : X → E) : 0 ≤ ∑ x ∈ C, ∑ y ∈ C, inner ℝ (q x) (q y)

theorem MetricCodes.projection_certificate_mul {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D d : ℕ} (P : ProjectionFamily X D d) (C : Finset X) (t : X → X → ℝ) (q : X → E) {s lam : ℝ} (hd : 0 < d) (hs : s < 1) (hgap : s < lam) (hdiag : ∀ x ∈ C, t x x = 1) (hsep : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → t x y ≤ s) (hgram : ∀ x ∈ C, ∀ y ∈ C, inner ℝ (q x) (q y) = (t x y - lam) * P.overlap x y) : ↑C.card * (lam - s) * ↑d ≤ (1 - s) * ↑D

theorem MetricCodes.projection_certificate {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D d : ℕ} (P : ProjectionFamily X D d) (C : Finset X) (t : X → X → ℝ) (q : X → E) {s lam : ℝ} (hd : 0 < d) (hs : s < 1) (hgap : s < lam) (hdiag : ∀ x ∈ C, t x x = 1) (hsep : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → t x y ≤ s) (hgram : ∀ x ∈ C, ∀ y ∈ C, inner ℝ (q x) (q y) = (t x y - lam) * P.overlap x y) : ↑C.card ≤ (1 - s) / (lam - s) * (↑D / ↑d)

def MetricCodes.Boolean.sign (b : Bool) : ℝ

The sign used in the binary-code argument.

Equations

• MetricCodes.Boolean.sign b = if b = true then -1 else 1

@[simp]

theorem MetricCodes.Boolean.sign_mul_self (b : Bool) : sign b * sign b = 1

def MetricCodes.Boolean.character {n : ℕ} (x : BinaryWord n) (S : Finset (Fin n)) : ℝ

The Boolean character given by the product of the signs of x on S.

Equations

• MetricCodes.Boolean.character x S = ∏ a ∈ S, MetricCodes.Boolean.sign (x a)

@[simp]

theorem MetricCodes.Boolean.character_mul_self {n : ℕ} (x : BinaryWord n) (S : Finset (Fin n)) : character x S * character x S = 1

def MetricCodes.Boolean.twist {n : ℕ} (x : BinaryWord n) (f : Function n) (S : Finset (Fin n)) : ℝ

Multiply a function pointwise by the Boolean character of x.

Equations

• MetricCodes.Boolean.twist x f S = MetricCodes.Boolean.character x S * f S

theorem MetricCodes.Boolean.twist_smul {n : ℕ} (x : BinaryWord n) (c : ℝ) (f : Function n) : twist x (c • f) = c • twist x f

theorem MetricCodes.Boolean.dot_twist {n : ℕ} (x : BinaryWord n) (f g : Function n) : dot (twist x f) (twist x g) = dot f g

theorem MetricCodes.Boolean.IsLevel.twist {n k : ℕ} {f : Function n} (hf : IsLevel k f) (x : BinaryWord n) : IsLevel k (Boolean.twist x f)

@[reducible, inline]

abbrev MetricCodes.Boolean.CoordinateFunction (n : ℕ) : Type

The coordinate function used in the binary-code argument.

Equations

• MetricCodes.Boolean.CoordinateFunction n = (Fin n → MetricCodes.Boolean.Function n)

def MetricCodes.Boolean.coordinateDot {n : ℕ} (f g : CoordinateFunction n) : ℝ

The coordinate dot used in the binary-code argument.

Equations

• MetricCodes.Boolean.coordinateDot f g = ∑ a : Fin n, MetricCodes.Boolean.dot (f a) (g a)

noncomputable def MetricCodes.Boolean.deleteChannel {n : ℕ} (i : ℕ) (f : Function n) : CoordinateFunction n

The delete channel used in the binary-code argument.

Equations

• MetricCodes.Boolean.deleteChannel i f a = (√↑i)⁻¹ • MetricCodes.Boolean.lowerAt a f

noncomputable def MetricCodes.Boolean.addChannel {n : ℕ} (i : ℕ) (f : Function n) : CoordinateFunction n

The coordinate raising channels scaled by the inverse square root of n - i.

Equations

• MetricCodes.Boolean.addChannel i f a = (√(↑n - ↑i))⁻¹ • MetricCodes.Boolean.raiseAt a f

theorem MetricCodes.Boolean.sum_not_mem_indicator {n : ℕ} (S : Finset (Fin n)) (z : ℝ) : (∑ a : Fin n, if a ∈ S then 0 else z) = (↑n - ↑S.card) * z

theorem MetricCodes.Boolean.sum_dot_lowerAt {n : ℕ} (f g : Function n) : ∑ a : Fin n, dot (lowerAt a f) (lowerAt a g) = ∑ S : Finset (Fin n), ↑S.card * f S * g S

theorem MetricCodes.Boolean.sum_dot_raiseAt {n : ℕ} (f g : Function n) : ∑ a : Fin n, dot (raiseAt a f) (raiseAt a g) = ∑ S : Finset (Fin n), (↑n - ↑S.card) * f S * g S

theorem MetricCodes.Boolean.sum_dot_lowerAt_of_level {n i : ℕ} (f g : Function n) (hf : IsLevel i f) : ∑ a : Fin n, dot (lowerAt a f) (lowerAt a g) = ↑i * dot f g

theorem MetricCodes.Boolean.sum_dot_raiseAt_of_level {n i : ℕ} (f g : Function n) (hf : IsLevel i f) : ∑ a : Fin n, dot (raiseAt a f) (raiseAt a g) = (↑n - ↑i) * dot f g

theorem MetricCodes.Boolean.dot_smul_left {n : ℕ} (f g : Function n) (c : ℝ) : dot (c • f) g = c * dot f g

theorem MetricCodes.Boolean.dot_add_right {n : ℕ} (f g h : Function n) : dot f (g + h) = dot f g + dot f h

theorem MetricCodes.Boolean.normSq_raise_of_level {n i : ℕ} (f : Function n) (hf : IsLevel i f) : dot (raise f) (raise f) = dot (lower f) (lower f) + (↑n - 2 * ↑i) * dot f f

theorem MetricCodes.Boolean.raise_eq_zero_iff_of_level {n i : ℕ} (hi : 2 * i < n) (f : Function n) (hf : IsLevel i f) : raise f = 0 ↔ f = 0

@[reducible, inline]

abbrev MetricCodes.Boolean.LayerFunction (n k : ℕ) : Type

The layer function used in the binary-code argument.

Equations

• MetricCodes.Boolean.LayerFunction n k = (MetricCodes.Boolean.Level n k → ℝ)

def MetricCodes.Boolean.layerExtend {n k : ℕ} (f : LayerFunction n k) : Function n

The layer extend used in the binary-code argument.

Equations

• MetricCodes.Boolean.layerExtend f S = if h : S.card = k then f ⟨S, h⟩ else 0

def MetricCodes.Boolean.layerRestrict {n : ℕ} (k : ℕ) (f : Function n) : LayerFunction n k

The layer restrict used in the binary-code argument.

Equations

• MetricCodes.Boolean.layerRestrict k f S = f ↑S

theorem MetricCodes.Boolean.isLevel_layerExtend {n k : ℕ} (f : LayerFunction n k) : IsLevel k (layerExtend f)

@[simp]

theorem MetricCodes.Boolean.layerRestrict_layerExtend {n k : ℕ} (f : LayerFunction n k) : layerRestrict k (layerExtend f) = f

theorem MetricCodes.Boolean.layerExtend_layerRestrict_of_level {n k : ℕ} (f : Function n) (hf : IsLevel k f) : layerExtend (layerRestrict k f) = f

theorem MetricCodes.Boolean.layerExtend_injective {n k : ℕ} : Function.Injective layerExtend

def MetricCodes.Boolean.layerExtendLinear (n k : ℕ) : LayerFunction n k →ₗ[ℝ] Function n

Extend a function on the kth layer by zero, bundled as a linear map.

Equations

• MetricCodes.Boolean.layerExtendLinear n k = { toFun := MetricCodes.Boolean.layerExtend, map_add' := ⋯, map_smul' := ⋯ }

def MetricCodes.Boolean.layerRestrictLinear (n k : ℕ) : Function n →ₗ[ℝ] LayerFunction n k

Restrict a function to the kth layer, bundled as a linear map.

Equations

• MetricCodes.Boolean.layerRestrictLinear n k = { toFun := MetricCodes.Boolean.layerRestrict k, map_add' := ⋯, map_smul' := ⋯ }

def MetricCodes.Boolean.layerUp (n k : ℕ) : LayerFunction n k →ₗ[ℝ] LayerFunction n (k + 1)

The raising map from layer k to layer k + 1, obtained by extending and restricting.

Equations

• MetricCodes.Boolean.layerUp n k = MetricCodes.Boolean.layerRestrictLinear n (k + 1) ∘ₗ MetricCodes.Boolean.raiseLinear n ∘ₗ MetricCodes.Boolean.layerExtendLinear n k

def MetricCodes.Boolean.layerDown (n k : ℕ) : LayerFunction n (k + 1) →ₗ[ℝ] LayerFunction n k

The lowering map from layer k + 1 to layer k, obtained by extending and restricting.

Equations

• MetricCodes.Boolean.layerDown n k = MetricCodes.Boolean.layerRestrictLinear n k ∘ₗ MetricCodes.Boolean.lowerLinear n ∘ₗ MetricCodes.Boolean.layerExtendLinear n (k + 1)

@[simp]

theorem MetricCodes.Boolean.layerUp_apply {n k : ℕ} (f : LayerFunction n k) : (layerUp n k) f = layerRestrict (k + 1) (raise (layerExtend f))

@[simp]

theorem MetricCodes.Boolean.layerDown_apply {n k : ℕ} (f : LayerFunction n (k + 1)) : (layerDown n k) f = layerRestrict k (lower (layerExtend f))

theorem MetricCodes.Boolean.layerUp_injective {n k : ℕ} (hk : 2 * k < n) : Function.Injective ⇑(layerUp n k)

def MetricCodes.Boolean.layerDot {n k : ℕ} (f g : LayerFunction n k) : ℝ

The layer dot used in the binary-code argument.

Equations

• MetricCodes.Boolean.layerDot f g = ∑ S : MetricCodes.Boolean.Level n k, f S * g S

theorem MetricCodes.Boolean.dot_layerExtend {n k : ℕ} (f g : LayerFunction n k) : dot (layerExtend f) (layerExtend g) = layerDot f g

theorem MetricCodes.Boolean.layerUp_layerDown_adjoint {n k : ℕ} (f : LayerFunction n k) (g : LayerFunction n (k + 1)) : layerDot ((layerUp n k) f) g = layerDot f ((layerDown n k) g)

theorem MetricCodes.Boolean.layerUp_toMatrix_transpose (n k : ℕ) : LinearMap.toMatrix' (layerUp n k) = (LinearMap.toMatrix' (layerDown n k)).transpose

theorem MetricCodes.Boolean.layerUp_matrix_rank {n k : ℕ} (hk : 2 * k < n) : (LinearMap.toMatrix' (layerUp n k)).rank = n.choose k

theorem MetricCodes.Boolean.layerDown_matrix_rank {n k : ℕ} (hk : 2 * k < n) : (LinearMap.toMatrix' (layerDown n k)).rank = n.choose k

theorem MetricCodes.Boolean.layerDown_surjective {n k : ℕ} (hk : 2 * k < n) : Function.Surjective ⇑(layerDown n k)

theorem MetricCodes.Boolean.finrank_ker_layerDown {n k : ℕ} (hk : 2 * k < n) : Module.finrank ℝ ↥(layerDown n k).ker = n.choose (k + 1) - n.choose k

def MetricCodes.Boolean.harmonicLayer (n k : ℕ) : Submodule ℝ (LayerFunction n k)

The harmonic layer used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicLayer n 0 = ⊤
• MetricCodes.Boolean.harmonicLayer n k.succ = (MetricCodes.Boolean.layerDown n k).ker

theorem MetricCodes.Boolean.harmonicLayer_finrank (n k : ℕ) (hk : 2 * k ≤ n) : Module.finrank ℝ ↥(harmonicLayer n k) = hammingFibreDimension n k

theorem MetricCodes.Boolean.deleteChannel_isometry {n i : ℕ} (hi : 0 < i) (f g : Function n) (hf : IsLevel i f) : coordinateDot (deleteChannel i f) (deleteChannel i g) = dot f g

theorem MetricCodes.Boolean.addChannel_isometry {n i : ℕ} (hi : i < n) (f g : Function n) (hf : IsLevel i f) : coordinateDot (addChannel i f) (addChannel i g) = dot f g

theorem MetricCodes.Boolean.dot_lowerAt_raiseAt {n : ℕ} (a : Fin n) (f g : Function n) : dot (lowerAt a f) (raiseAt a g) = 0

theorem MetricCodes.Boolean.deleteChannel_orthogonal_addChannel {n : ℕ} (i j : ℕ) (f g : Function n) : coordinateDot (deleteChannel i f) (addChannel j g) = 0

def MetricCodes.Boolean.harmonicNormFactor (n k r : ℕ) : ℝ

The harmonic norm factor used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicNormFactor n k r = ∏ j ∈ Finset.range r, MetricCodes.Boolean.harmonicCoefficient n k (j + 1)

@[simp]

theorem MetricCodes.Boolean.harmonicNormFactor_zero (n k : ℕ) : harmonicNormFactor n k 0 = 1

theorem MetricCodes.Boolean.harmonicCoefficient_pos {n k r : ℕ} (hr : 0 < r) (hbound : 2 * k + r ≤ n) : 0 < harmonicCoefficient n k r

theorem MetricCodes.Boolean.harmonicNormFactor_pos {n k r : ℕ} (hbound : 2 * k + r ≤ n) : 0 < harmonicNormFactor n k r

theorem MetricCodes.Boolean.dot_raised_succ_of_harmonic {n k : ℕ} (f g : Function n) (hg : IsHarmonic k g) (r : ℕ) : dot (raised f (r + 1)) (raised g (r + 1)) = harmonicCoefficient n k (r + 1) * dot (raised f r) (raised g r)

theorem MetricCodes.Boolean.dot_raised_of_harmonic {n k : ℕ} (f g : Function n) (hg : IsHarmonic k g) (r : ℕ) : dot (raised f r) (raised g r) = harmonicNormFactor n k r * dot f g

noncomputable def MetricCodes.Boolean.harmonicEmbedding {n : ℕ} (k r : ℕ) (f : Function n) : Function n

The harmonic embedding used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicEmbedding k r f = (√(MetricCodes.Boolean.harmonicNormFactor n k r))⁻¹ • MetricCodes.Boolean.raised f r

noncomputable def MetricCodes.Boolean.wordHarmonicEmbedding {n : ℕ} (x : BinaryWord n) (k r : ℕ) (f : Function n) : Function n

The normalized harmonic embedding twisted by the Boolean character of x.

Equations

• MetricCodes.Boolean.wordHarmonicEmbedding x k r f = MetricCodes.Boolean.twist x (MetricCodes.Boolean.harmonicEmbedding k r f)

theorem MetricCodes.Boolean.harmonicEmbedding_isometry {n k : ℕ} (f g : Function n) (hg : IsHarmonic k g) (r : ℕ) (hbound : 2 * k + r ≤ n) : dot (harmonicEmbedding k r f) (harmonicEmbedding k r g) = dot f g

theorem MetricCodes.Boolean.wordHarmonicEmbedding_isometry {n k : ℕ} (x : BinaryWord n) (f g : Function n) (hg : IsHarmonic k g) (r : ℕ) (hbound : 2 * k + r ≤ n) : dot (wordHarmonicEmbedding x k r f) (wordHarmonicEmbedding x k r g) = dot f g

theorem MetricCodes.Boolean.IsLevel.harmonicEmbedding {n k : ℕ} {f : Function n} (hf : IsLevel k f) (r : ℕ) : IsLevel (k + r) (Boolean.harmonicEmbedding k r f)

theorem MetricCodes.Boolean.IsLevel.wordHarmonicEmbedding {n k : ℕ} {f : Function n} (hf : IsLevel k f) (x : BinaryWord n) (r : ℕ) : IsLevel (k + r) (Boolean.wordHarmonicEmbedding x k r f)

theorem MetricCodes.Boolean.mem_harmonicLayer_iff {n k : ℕ} (f : LayerFunction n k) : f ∈ harmonicLayer n k ↔ IsHarmonic k (layerExtend f)

@[reducible, inline]

abbrev MetricCodes.Boolean.EuclideanLayer (n k : ℕ) : Type

The euclidean layer used in the binary-code argument.

Equations

• MetricCodes.Boolean.EuclideanLayer n k = EuclideanSpace ℝ (MetricCodes.Boolean.Level n k)

def MetricCodes.Boolean.harmonicEuclideanLayer (n k : ℕ) : Submodule ℝ (EuclideanLayer n k)

The harmonic euclidean layer used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicEuclideanLayer n k = Submodule.map (↑(WithLp.linearEquiv 2 ℝ (MetricCodes.Boolean.LayerFunction n k)).symm) (MetricCodes.Boolean.harmonicLayer n k)

theorem MetricCodes.Boolean.harmonicEuclideanLayer_finrank (n k : ℕ) (hk : 2 * k ≤ n) : Module.finrank ℝ ↥(harmonicEuclideanLayer n k) = hammingFibreDimension n k

noncomputable def MetricCodes.Boolean.harmonicOrthonormalBasis (n k : ℕ) (hk : 2 * k ≤ n) : OrthonormalBasis (Fin (hammingFibreDimension n k)) ℝ ↥(harmonicEuclideanLayer n k)

The harmonic orthonormal basis used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicOrthonormalBasis n k hk = (stdOrthonormalBasis ℝ ↥(MetricCodes.Boolean.harmonicEuclideanLayer n k)).reindex (finCongr ⋯)

noncomputable def MetricCodes.Boolean.harmonicBasisFunction (n k : ℕ) (hk : 2 * k ≤ n) (p : Fin (hammingFibreDimension n k)) : Function n

The harmonic basis function used in the binary-code argument.

Equations

• MetricCodes.Boolean.harmonicBasisFunction n k hk p = MetricCodes.Boolean.layerExtend (↑((MetricCodes.Boolean.harmonicOrthonormalBasis n k hk) p)).ofLp

theorem MetricCodes.Boolean.harmonicBasisFunction_isHarmonic (n k : ℕ) (hk : 2 * k ≤ n) (p : Fin (hammingFibreDimension n k)) : IsHarmonic k (harmonicBasisFunction n k hk p)

def MetricCodes.Boolean.hammingWindowDimension (n k L : ℕ) : ℕ

The sum of the layer dimensions over the offsets in Fin (L - k + 1).

Equations

• MetricCodes.Boolean.hammingWindowDimension n k L = ∑ j ∈ Finset.range (L - k + 1), n.choose (k + j)

@[reducible, inline]

abbrev MetricCodes.Boolean.HammingWindowIndex (n k L : ℕ) : Type

Indices consisting of a window offset and a subset in its corresponding Hamming layer.

Equations

• MetricCodes.Boolean.HammingWindowIndex n k L = ((j : Fin (L - k + 1)) × MetricCodes.Boolean.Level n (k + ↑j))

theorem MetricCodes.Boolean.hammingWindowIndex_card (n k L : ℕ) : Fintype.card (HammingWindowIndex n k L) = hammingWindowDimension n k L

noncomputable def MetricCodes.Boolean.hammingWindowIndexEquiv (n k L : ℕ) : HammingWindowIndex n k L ≃ Fin (hammingWindowDimension n k L)

Enumerate the Hamming window indices by their total dimension.

Equations

• MetricCodes.Boolean.hammingWindowIndexEquiv n k L = Fintype.equivOfCardEq ⋯

noncomputable def MetricCodes.Boolean.hammingRecurrenceWeight (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (j : Fin (L - k + 1)) : ℝ

A recurrence coordinate weighted by the square root of its Hamming layer dimension.

Equations

• MetricCodes.Boolean.hammingRecurrenceWeight n k L v j = √↑(n.choose (k + ↑j)) * v.ofLp j

noncomputable def MetricCodes.Boolean.hammingRecurrenceNormalization (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) : ℝ

The sum of the dimension-weighted Hamming recurrence coordinates.

Equations

• MetricCodes.Boolean.hammingRecurrenceNormalization n k L v = ∑ j : Fin (L - k + 1), MetricCodes.Boolean.hammingRecurrenceWeight n k L v j

noncomputable def MetricCodes.Boolean.hammingFibreAmplitude (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (j : Fin (L - k + 1)) : ℝ

The square root of a normalized Hamming recurrence weight, used as a fibre amplitude.

Equations

• MetricCodes.Boolean.hammingFibreAmplitude n k L v j = √(MetricCodes.Boolean.hammingRecurrenceWeight n k L v j / MetricCodes.Boolean.hammingRecurrenceNormalization n k L v)

theorem MetricCodes.Boolean.hammingRecurrenceWeight_nonneg (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) (j : Fin (L - k + 1)) : 0 ≤ hammingRecurrenceWeight n k L v j

theorem MetricCodes.Boolean.hammingRecurrenceNormalization_pos {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) : 0 < hammingRecurrenceNormalization n k L v

theorem MetricCodes.Boolean.hammingFibreAmplitude_sq {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) (j : Fin (L - k + 1)) : hammingFibreAmplitude n k L v j ^ 2 = hammingRecurrenceWeight n k L v j / hammingRecurrenceNormalization n k L v

theorem MetricCodes.Boolean.hammingFibreAmplitude_sq_sum {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) : ∑ j : Fin (L - k + 1), hammingFibreAmplitude n k L v j ^ 2 = 1

theorem MetricCodes.Boolean.harmonicBasisFunction_dot (n k : ℕ) (hk : 2 * k ≤ n) (p q : Fin (hammingFibreDimension n k)) : dot (harmonicBasisFunction n k hk p) (harmonicBasisFunction n k hk q) = if p = q then 1 else 0

theorem MetricCodes.Boolean.dot_eq_layerDot_of_level {n i : ℕ} (f g : Function n) (hf : IsLevel i f) (hg : IsLevel i g) : dot f g = layerDot (layerRestrict i f) (layerRestrict i g)

noncomputable def MetricCodes.Boolean.hammingWindowFibreMatrix (n k L : ℕ) (hk : 2 * k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (x : BinaryWord n) : Matrix (HammingWindowIndex n k L) (Fin (hammingFibreDimension n k)) ℝ

The matrix of twisted harmonic basis embeddings weighted by their window fibre amplitudes.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.hammingWindowFibreMatrix_transpose_mul {n k L : ℕ} (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) (x : BinaryWord n) : (hammingWindowFibreMatrix n k L hk v x).transpose * hammingWindowFibreMatrix n k L hk v x = 1

noncomputable def MetricCodes.Boolean.hammingFibreMatrix (n k L : ℕ) (hk : 2 * k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (x : BinaryWord n) : Matrix (Fin (hammingWindowDimension n k L)) (Fin (hammingFibreDimension n k)) ℝ

The Hamming window fibre matrix with its rows enumerated by the window dimension.

Equations

• MetricCodes.Boolean.hammingFibreMatrix n k L hk v x i p = MetricCodes.Boolean.hammingWindowFibreMatrix n k L hk v x ((MetricCodes.Boolean.hammingWindowIndexEquiv n k L).symm i) p

theorem MetricCodes.Boolean.hammingFibreMatrix_transpose_mul {n k L : ℕ} (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) (x : BinaryWord n) : (hammingFibreMatrix n k L hk v x).transpose * hammingFibreMatrix n k L hk v x = 1

noncomputable def MetricCodes.Boolean.hammingProjectionFamily {n k L : ℕ} (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (j : Fin (L - k + 1)), 0 ≤ v.ofLp j) : ProjectionFamily (BinaryWord n) (hammingWindowDimension n k L) (hammingFibreDimension n k)

The hamming projection family used in the binary-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.sign_mul_eq_difference_indicator (b c : Bool) : sign b * sign c = 1 - 2 * if b ≠ c then 1 else 0

theorem MetricCodes.Boolean.sum_sign_mul_eq_hammingDist {n : ℕ} (x y : BinaryWord n) : ∑ a : Fin n, sign (x a) * sign (y a) = ↑n - 2 * ↑(hammingDist x y)

noncomputable def MetricCodes.Boolean.hammingAxis {n : ℕ} (x : BinaryWord n) : EuclideanSpace ℝ (Fin n)

The Euclidean sign vector of a binary word, scaled by the inverse square root of n.

Equations

• MetricCodes.Boolean.hammingAxis x = WithLp.toLp 2 fun (a : Fin n) => (√↑n)⁻¹ * MetricCodes.Boolean.sign (x a)

theorem MetricCodes.Boolean.hammingAxis_inner {n : ℕ} (hn : 0 < n) (x y : BinaryWord n) : inner ℝ (hammingAxis x) (hammingAxis y) = hammingCorrelation x y

theorem MetricCodes.Boolean.character_insert {n : ℕ} (x : BinaryWord n) (a : Fin n) (S : Finset (Fin n)) (ha : a ∉ S) : character x (insert a S) = sign (x a) * character x S

theorem MetricCodes.Boolean.character_erase {n : ℕ} (x : BinaryWord n) (a : Fin n) (S : Finset (Fin n)) (ha : a ∈ S) : character x S = sign (x a) * character x (S.erase a)

theorem MetricCodes.Boolean.lowerAt_twist {n : ℕ} (x : BinaryWord n) (a : Fin n) (f : Function n) : lowerAt a (twist x f) = sign (x a) • twist x (lowerAt a f)

theorem MetricCodes.Boolean.raiseAt_twist {n : ℕ} (x : BinaryWord n) (a : Fin n) (f : Function n) : raiseAt a (twist x f) = sign (x a) • twist x (raiseAt a f)

def MetricCodes.Boolean.matrixHilbertSchmidtFeature {ι : Type u_1} {ρ : Type u_2} (A : Matrix ι ρ ℝ) : EuclideanSpace ℝ (ι × ρ)

The Euclidean vector of matrix entries used to express the Hilbert–Schmidt inner product.

Equations

• MetricCodes.Boolean.matrixHilbertSchmidtFeature A = WithLp.toLp 2 fun (p : ι × ρ) => A p.1 p.2

theorem MetricCodes.Boolean.matrixHilbertSchmidtFeature_inner {ι : Type u_1} {ρ : Type u_2} [Fintype ι] [Fintype ρ] (A B : Matrix ι ρ ℝ) : inner ℝ (matrixHilbertSchmidtFeature A) (matrixHilbertSchmidtFeature B) = (A.transpose * B).trace

@[simp]

theorem MetricCodes.Boolean.matrixHilbertSchmidtFeature_sub {ι : Type u_1} {ρ : Type u_2} (A B : Matrix ι ρ ℝ) : matrixHilbertSchmidtFeature (A - B) = matrixHilbertSchmidtFeature A - matrixHilbertSchmidtFeature B

@[simp]

theorem MetricCodes.Boolean.matrixHilbertSchmidtFeature_smul {ι : Type u_1} {ρ : Type u_2} (c : ℝ) (A : Matrix ι ρ ℝ) : matrixHilbertSchmidtFeature (c • A) = c • matrixHilbertSchmidtFeature A

def MetricCodes.Boolean.matrixAxisLift {κ : Type u_1} {ι : Type u_2} {ρ : Type u_3} (z : κ → ℝ) (A : Matrix ι ρ ℝ) : Matrix (κ × ι) ρ ℝ

The matrix axis lift used in the binary-code argument.

Equations

• MetricCodes.Boolean.matrixAxisLift z A p j = z p.1 * A p.2 j

theorem MetricCodes.Boolean.matrixAxisLift_transpose_mul {κ : Type u_1} {ι : Type u_2} {ρ : Type u_3} [Fintype κ] [Fintype ι] (z w : κ → ℝ) (A B : Matrix ι ρ ℝ) : (matrixAxisLift z A).transpose * matrixAxisLift w B = (∑ a : κ, z a * w a) • (A.transpose * B)

def MetricCodes.Boolean.matrixAxisResidual {X : Type u_1} {κ : Type u_2} {D d : ℕ} (P : ProjectionFamily X D d) (axis : X → κ → ℝ) (B : Matrix (κ × Fin D) (Fin D) ℝ) (c : ℝ) (x : X) : Matrix (κ × Fin D) (Fin D) ℝ

The axis-lifted projection minus the scaled channel image of that projection.

Equations

• MetricCodes.Boolean.matrixAxisResidual P axis B c x = MetricCodes.Boolean.matrixAxisLift (axis x) (P.projection x) - c • (B * P.projection x)

def MetricCodes.Boolean.matrixAxisGramFeature {X : Type u_1} {κ : Type u_2} {D d : ℕ} (P : ProjectionFamily X D d) (axis : X → κ → ℝ) (B : Matrix (κ × Fin D) (Fin D) ℝ) (c : ℝ) (x : X) : EuclideanSpace ℝ ((κ × Fin D) × Fin D)

The matrix axis gram feature used in the binary-code argument.

Equations

• MetricCodes.Boolean.matrixAxisGramFeature P axis B c x = MetricCodes.Boolean.matrixHilbertSchmidtFeature (MetricCodes.Boolean.matrixAxisResidual P axis B c x)

theorem MetricCodes.Boolean.matrixAxisResidual_gram {X : Type u_1} {κ : Type u_2} [Fintype κ] {D d : ℕ} (P : ProjectionFamily X D d) (axis : X → κ → ℝ) (B : Matrix (κ × Fin D) (Fin D) ℝ) (c lam : ℝ) (hB : B.transpose * B = 1) (haxis : ∀ (x : X), B.transpose * matrixAxisLift (axis x) (P.projection x) = c • P.projection x) (hsq : c ^ 2 = lam) (x y : X) : inner ℝ (matrixAxisGramFeature P axis B c x) (matrixAxisGramFeature P axis B c y) = (∑ a : κ, axis x a * axis y a - lam) * P.overlap x y

@[simp]

theorem MetricCodes.Boolean.harmonicNormFactor_succ (n k r : ℕ) : harmonicNormFactor n k (r + 1) = harmonicNormFactor n k r * harmonicCoefficient n k (r + 1)

theorem MetricCodes.Boolean.raise_harmonicEmbedding {n k : ℕ} (f : Function n) (r : ℕ) (hbound : 2 * k + (r + 1) ≤ n) : raise (harmonicEmbedding k r f) = √(harmonicCoefficient n k (r + 1)) • harmonicEmbedding k (r + 1) f

theorem MetricCodes.Boolean.lower_harmonicEmbedding {n k : ℕ} (f : Function n) (hf : IsHarmonic k f) (r : ℕ) (hbound : 2 * k + (r + 1) ≤ n) : lower (harmonicEmbedding k (r + 1) f) = √(harmonicCoefficient n k (r + 1)) • harmonicEmbedding k r f

noncomputable def MetricCodes.Boolean.hammingSourceChannelCoefficient (n k L : ℕ) (m i : Fin (L - k + 1)) : ℝ

The Hamming Jacobi entry rescaled by the square roots of the source and target layer dimensions.

Equations

• MetricCodes.Boolean.hammingSourceChannelCoefficient n k L m i = MetricCodes.hammingJacobiMatrix n k L m i * √↑(n.choose (k + ↑m)) / √↑(n.choose (k + ↑i))

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_mul_sqrt_choose {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (m i : Fin (L - k + 1)) : hammingSourceChannelCoefficient n k L m i * √↑(n.choose (k + ↑i)) = hammingJacobiMatrix n k L m i * √↑(n.choose (k + ↑m))

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_nonneg {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (m i : Fin (L - k + 1)) : 0 ≤ hammingSourceChannelCoefficient n k L m i

theorem MetricCodes.Boolean.hammingRecurrenceWeight_eigenrecurrence {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (lam : ℝ) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (m : Fin (L - k + 1)) : ∑ i : Fin (L - k + 1), hammingSourceChannelCoefficient n k L m i * hammingRecurrenceWeight n k L v i = lam * hammingRecurrenceWeight n k L v m

theorem MetricCodes.Boolean.hammingRecurrenceWeight_pos_of_pos {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (i : Fin (L - k + 1)) : 0 < hammingRecurrenceWeight n k L v i

theorem MetricCodes.Boolean.hammingFibreAmplitude_pos_of_pos {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (i : Fin (L - k + 1)) : 0 < hammingFibreAmplitude n k L v i

noncomputable def MetricCodes.Boolean.hammingAdjacentBlockCoefficient (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (lam : ℝ) (target source : Fin (L - k + 1)) : ℝ

The square-root weight for an adjacent channel block, normalized by the eigenvalue and source recurrence weight.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.hammingAdjacentBlockCoefficient_sq {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (target source : Fin (L - k + 1)) : hammingAdjacentBlockCoefficient n k L v lam target source ^ 2 = hammingSourceChannelCoefficient n k L source target * hammingRecurrenceWeight n k L v target / (lam * hammingRecurrenceWeight n k L v source)

theorem MetricCodes.Boolean.hammingAdjacentBlockCoefficient_sq_sum {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (source : Fin (L - k + 1)) : ∑ target : Fin (L - k + 1), hammingAdjacentBlockCoefficient n k L v lam target source ^ 2 = 1

theorem MetricCodes.Boolean.hammingAdjacentBlockCoefficient_amplitude_identity {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (target source : Fin (L - k + 1)) : hammingAdjacentBlockCoefficient n k L v lam target source * hammingFibreAmplitude n k L v target * √(hammingSourceChannelCoefficient n k L source target) = hammingAdjacentBlockCoefficient n k L v lam target source ^ 2 * √lam * hammingFibreAmplitude n k L v source

theorem MetricCodes.Boolean.hammingAdjacentBlockCoefficient_amplitude_sum {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (source : Fin (L - k + 1)) : ∑ target : Fin (L - k + 1), hammingAdjacentBlockCoefficient n k L v lam target source * hammingFibreAmplitude n k L v target * √(hammingSourceChannelCoefficient n k L source target) = √lam * hammingFibreAmplitude n k L v source

theorem MetricCodes.Boolean.IsLevel.smul {n i : ℕ} {f : Function n} (hf : IsLevel i f) (c : ℝ) : IsLevel i (c • f)

theorem MetricCodes.Boolean.IsLevel.lowerAt {n i : ℕ} {f : Function n} (hf : IsLevel (i + 1) f) (a : Fin n) : IsLevel i (Boolean.lowerAt a f)

theorem MetricCodes.Boolean.IsLevel.raiseAt {n i : ℕ} {f : Function n} (hf : IsLevel i f) (a : Fin n) : IsLevel (i + 1) (Boolean.raiseAt a f)

def MetricCodes.Boolean.hammingWindowBasis (n k L : ℕ) (T : HammingWindowIndex n k L) : Function n

The indicator function of the subset specified by a Hamming window index.

Equations

• MetricCodes.Boolean.hammingWindowBasis n k L T S = if S = ↑T.snd then 1 else 0

theorem MetricCodes.Boolean.isLevel_hammingWindowBasis (n k L : ℕ) (T : HammingWindowIndex n k L) : IsLevel (k + ↑T.fst) (hammingWindowBasis n k L T)

theorem MetricCodes.Boolean.dot_hammingWindowBasis (n k L : ℕ) (S T : HammingWindowIndex n k L) : dot (hammingWindowBasis n k L S) (hammingWindowBasis n k L T) = if ↑S.snd = ↑T.snd then 1 else 0

noncomputable def MetricCodes.Boolean.hammingAdjacentChannel (n k L : ℕ) (target source : Fin (L - k + 1)) (f : Function n) : CoordinateFunction n

The deletion or insertion channel between adjacent window levels, and zero otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.coordinateDot_comm {n : ℕ} (f g : CoordinateFunction n) : coordinateDot f g = coordinateDot g f

theorem MetricCodes.Boolean.hammingAdjacentChannel_isometry {n k L : ℕ} (hkL : k ≤ L) (hLn : L + k ≤ n) (target source : Fin (L - k + 1)) (hadjacent : ↑target + 1 = ↑source ∨ ↑source + 1 = ↑target) (f g : Function n) (hf : IsLevel (k + ↑source) f) : coordinateDot (hammingAdjacentChannel n k L target source f) (hammingAdjacentChannel n k L target source g) = dot f g

theorem MetricCodes.Boolean.hammingAdjacentChannel_orthogonal (n k L : ℕ) (target source other : Fin (L - k + 1)) (hne : source ≠ other) (f g : Function n) : coordinateDot (hammingAdjacentChannel n k L target source f) (hammingAdjacentChannel n k L target other g) = 0

theorem MetricCodes.Boolean.hammingAdjacentChannel_isLevel (n k L : ℕ) (target source : Fin (L - k + 1)) (f : Function n) (hf : IsLevel (k + ↑source) f) (a : Fin n) : IsLevel (k + ↑target) (hammingAdjacentChannel n k L target source f a)

theorem MetricCodes.Boolean.hammingAdjacentChannel_restricted_coordinateDot (n k L : ℕ) (target source other : Fin (L - k + 1)) (f g : Function n) (hf : IsLevel (k + ↑source) f) (hg : IsLevel (k + ↑other) g) : ∑ a : Fin n, ∑ S : Level n (k + ↑target), hammingAdjacentChannel n k L target source f a ↑S * hammingAdjacentChannel n k L target other g a ↑S = coordinateDot (hammingAdjacentChannel n k L target source f) (hammingAdjacentChannel n k L target other g)

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_eq_zero_of_not_adjacent (n k L : ℕ) (source target : Fin (L - k + 1)) (hnot : ¬(↑target + 1 = ↑source ∨ ↑source + 1 = ↑target)) : hammingSourceChannelCoefficient n k L source target = 0

noncomputable def MetricCodes.Boolean.hammingWindowChannelMatrix (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (lam : ℝ) : Matrix (Fin n × HammingWindowIndex n k L) (HammingWindowIndex n k L) ℝ

The weighted adjacent-channel matrix in the Hamming window basis.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.hammingWindowChannelMatrix_pairing (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (lam : ℝ) (Q R : HammingWindowIndex n k L) : ∑ p : Fin n × HammingWindowIndex n k L, hammingWindowChannelMatrix n k L v lam p Q * hammingWindowChannelMatrix n k L v lam p R = ∑ target : Fin (L - k + 1), hammingAdjacentBlockCoefficient n k L v lam target Q.fst * hammingAdjacentBlockCoefficient n k L v lam target R.fst * coordinateDot (hammingAdjacentChannel n k L target Q.fst (hammingWindowBasis n k L Q)) (hammingAdjacentChannel n k L target R.fst (hammingWindowBasis n k L R))

theorem MetricCodes.Boolean.hammingWindowChannelMatrix_transpose_mul {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) : (hammingWindowChannelMatrix n k L v lam).transpose * hammingWindowChannelMatrix n k L v lam = 1

noncomputable def MetricCodes.Boolean.hammingChannelMatrix (n k L : ℕ) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (lam : ℝ) : Matrix (Fin n × Fin (hammingWindowDimension n k L)) (Fin (hammingWindowDimension n k L)) ℝ

The Hamming window channel matrix with both window indices enumerated by their total dimension.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.hammingChannelMatrix_transpose_mul {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) : (hammingChannelMatrix n k L v lam).transpose * hammingChannelMatrix n k L v lam = 1

theorem MetricCodes.Boolean.hammingPositiveRadicalSymmetrization {d e a b N r : ℝ} (hd : 0 < d) (he : 0 < e) (ha : 0 < a) (hb : 0 < b) (hN : 0 < N) (hcross : d * b = e * a) : r / (N * a) * √d = r / (N * √(a * b)) * √e

noncomputable def MetricCodes.Boolean.hammingDeletionChannelSquare (n k i : ℕ) : ℝ

The squared deletion-channel coefficient relating levels i and i + 1 in harmonic degree k.

Equations

• MetricCodes.Boolean.hammingDeletionChannelSquare n k i = (↑i - ↑k + 1) * (↑n - ↑i - ↑k) / (↑n * (↑i + 1))

noncomputable def MetricCodes.Boolean.hammingInsertionChannelSquare (n k i : ℕ) : ℝ

The squared insertion-channel coefficient relating levels i and i + 1 in harmonic degree k.

Equations

• MetricCodes.Boolean.hammingInsertionChannelSquare n k i = (↑i - ↑k + 1) * (↑n - ↑i - ↑k) / (↑n * (↑n - ↑i))

theorem MetricCodes.Boolean.hammingDeletionChannelSquare_mul_sqrt_choose {n k i : ℕ} (hn : 0 < n) : k ≤ i → ∀ (hboundary : i + k < n), hammingDeletionChannelSquare n k i * √↑(n.choose i) = hammingJacobiEntry n k i * √↑(n.choose (i + 1))

theorem MetricCodes.Boolean.hammingInsertionChannelSquare_mul_sqrt_choose {n k i : ℕ} (hn : 0 < n) : k ≤ i → ∀ (hboundary : i + k < n), hammingInsertionChannelSquare n k i * √↑(n.choose (i + 1)) = hammingJacobiEntry n k i * √↑(n.choose i)

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_eq_deletion {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (source target : Fin (L - k + 1)) (hadjacent : ↑target + 1 = ↑source) : hammingSourceChannelCoefficient n k L source target = hammingDeletionChannelSquare n k (k + ↑target)

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_eq_insertion {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (source target : Fin (L - k + 1)) (hadjacent : ↑source + 1 = ↑target) : hammingSourceChannelCoefficient n k L source target = hammingInsertionChannelSquare n k (k + ↑source)

theorem MetricCodes.Boolean.dot_lowerAt_eq_raiseAt {n : ℕ} (a : Fin n) (f g : Function n) : dot (lowerAt a f) g = dot f (raiseAt a g)

theorem MetricCodes.Boolean.sum_dot_twist_raiseAt {n : ℕ} (x : BinaryWord n) (f g : Function n) : ∑ a : Fin n, dot f (twist x (raiseAt a g)) = dot f (twist x (raise g))

theorem MetricCodes.Boolean.sum_dot_twist_lowerAt {n : ℕ} (x : BinaryWord n) (f g : Function n) : ∑ a : Fin n, dot f (twist x (lowerAt a g)) = dot f (twist x (lower g))

noncomputable def MetricCodes.Boolean.hammingAxisTensor {n : ℕ} (x : BinaryWord n) (f : Function n) : CoordinateFunction n

The coordinate-valued function obtained by tensoring f with the Hamming axis of x.

Equations

• MetricCodes.Boolean.hammingAxisTensor x f a = (MetricCodes.Boolean.hammingAxis x).ofLp a • f

theorem MetricCodes.Boolean.coordinateDot_deleteChannel_hammingAxisTensor {n : ℕ} (i : ℕ) (x : BinaryWord n) (f g : Function n) : coordinateDot (deleteChannel i f) (hammingAxisTensor x (twist x g)) = (√↑i)⁻¹ * (√↑n)⁻¹ * dot f (twist x (raise g))

theorem MetricCodes.Boolean.coordinateDot_addChannel_hammingAxisTensor {n : ℕ} (i : ℕ) (x : BinaryWord n) (f g : Function n) : coordinateDot (addChannel i f) (hammingAxisTensor x (twist x g)) = (√(↑n - ↑i))⁻¹ * (√↑n)⁻¹ * dot f (twist x (lower g))

theorem MetricCodes.Boolean.hammingSqrtDivProduct {r a b : ℝ} (hr : 0 ≤ r) (ha : 0 < a) (hb : 0 < b) : √(r / (a * b)) = (√a)⁻¹ * (√b)⁻¹ * √r

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_sqrt_deletion {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (source target : Fin (L - k + 1)) (hadjacent : ↑target + 1 = ↑source) : √(hammingSourceChannelCoefficient n k L source target) = (√↑n)⁻¹ * (√(↑k + ↑↑source))⁻¹ * √(harmonicCoefficient n k ↑source)

theorem MetricCodes.Boolean.hammingSourceChannelCoefficient_sqrt_insertion {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (source target : Fin (L - k + 1)) (hadjacent : ↑source + 1 = ↑target) : √(hammingSourceChannelCoefficient n k L source target) = (√↑n)⁻¹ * (√(↑n - (↑k + ↑↑source)))⁻¹ * √(harmonicCoefficient n k ↑target)

theorem MetricCodes.Boolean.hammingAdjacentChannel_axis_inner {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (x : BinaryWord n) (target source : Fin (L - k + 1)) (f h : Function n) (hh : IsHarmonic k h) : coordinateDot (hammingAdjacentChannel n k L target source f) (hammingAxisTensor x (wordHarmonicEmbedding x k (↑target) h)) = √(hammingSourceChannelCoefficient n k L source target) * dot f (wordHarmonicEmbedding x k (↑source) h)

theorem MetricCodes.Boolean.dot_hammingWindowBasis_apply (n k L : ℕ) (Q : HammingWindowIndex n k L) (f : Function n) : dot (hammingWindowBasis n k L Q) f = f ↑Q.snd

theorem MetricCodes.Boolean.hammingAdjacentChannel_restricted_axisDot (n k L : ℕ) (x : BinaryWord n) (target source : Fin (L - k + 1)) (f g : Function n) (hf : IsLevel (k + ↑source) f) (hg : IsLevel (k + ↑target) g) : ∑ a : Fin n, ∑ S : Level n (k + ↑target), hammingAdjacentChannel n k L target source f a ↑S * ((hammingAxis x).ofLp a * g ↑S) = coordinateDot (hammingAdjacentChannel n k L target source f) (hammingAxisTensor x g)

theorem MetricCodes.Boolean.hammingWindowChannelMatrix_transpose_axis_fibre {n k L : ℕ} (hn : 0 < n) (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (x : BinaryWord n) : (hammingWindowChannelMatrix n k L v lam).transpose * matrixAxisLift (fun (a : Fin n) => (hammingAxis x).ofLp a) (hammingWindowFibreMatrix n k L hk v x) = √lam • hammingWindowFibreMatrix n k L hk v x

theorem MetricCodes.Boolean.hammingChannelMatrix_transpose_axis_fibre {n k L : ℕ} (hn : 0 < n) (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (x : BinaryWord n) : (hammingChannelMatrix n k L v lam).transpose * matrixAxisLift (fun (a : Fin n) => (hammingAxis x).ofLp a) (hammingFibreMatrix n k L hk v x) = √lam • hammingFibreMatrix n k L hk v x

theorem MetricCodes.Boolean.matrixAxisLift_mul {κ : Type u_1} {ι : Type u_2} {ρ : Type u_3} {σ : Type u_4} [Fintype ρ] (z : κ → ℝ) (A : Matrix ι ρ ℝ) (C : Matrix ρ σ ℝ) : matrixAxisLift z (A * C) = matrixAxisLift z A * C

theorem MetricCodes.Boolean.hammingChannelMatrix_transpose_axis_projection {n k L : ℕ} (hn : 0 < n) (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (x : BinaryWord n) : (hammingChannelMatrix n k L v lam).transpose * matrixAxisLift (fun (a : Fin n) => (hammingAxis x).ofLp a) ((hammingProjectionFamily hk hkL hLn v hunit ⋯).projection x) = √lam • (hammingProjectionFamily hk hkL hLn v hunit ⋯).projection x

noncomputable def MetricCodes.Boolean.hammingProjectionGramFeature {n k L : ℕ} (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (x : BinaryWord n) : EuclideanSpace ℝ ((Fin n × Fin (hammingWindowDimension n k L)) × Fin (hammingWindowDimension n k L))

The hamming projection gram feature used in the binary-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Boolean.hammingProjectionGramFeature_inner {n k L : ℕ} (hn : 0 < n) (hk : 2 * k ≤ n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : EuclideanSpace ℝ (Fin (L - k + 1))) (hunit : ‖v‖ = 1) (hv : ∀ (i : Fin (L - k + 1)), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (Matrix.toEuclideanLin (hammingJacobiMatrix n k L)) v = lam • v) (x y : BinaryWord n) : inner ℝ (hammingProjectionGramFeature hk hkL hLn v hunit hv lam x) (hammingProjectionGramFeature hk hkL hLn v hunit hv lam y) = (hammingCorrelation x y - lam) * (hammingProjectionFamily hk hkL hLn v hunit ⋯).overlap x y

def MetricCodes.wordSupport {n : ℕ} (x : BinaryWord n) : Finset (Fin n)

The word support used in the metric-code argument.

Equations

• MetricCodes.wordSupport x = {i : Fin n | x i = true}

@[simp]

theorem MetricCodes.mem_wordSupport {n : ℕ} (x : BinaryWord n) (i : Fin n) : i ∈ wordSupport x ↔ x i = true

def MetricCodes.wordOfSupport {n : ℕ} (s : Finset (Fin n)) : BinaryWord n

The binary word whose true coordinates are exactly the elements of s.

Equations

• MetricCodes.wordOfSupport s i = decide (i ∈ s)

@[simp]

theorem MetricCodes.wordOfSupport_apply {n : ℕ} (s : Finset (Fin n)) (i : Fin n) : wordOfSupport s i = true ↔ i ∈ s

@[simp]

theorem MetricCodes.wordSupport_wordOfSupport {n : ℕ} (s : Finset (Fin n)) : wordSupport (wordOfSupport s) = s

@[simp]

theorem MetricCodes.wordOfSupport_wordSupport {n : ℕ} (x : BinaryWord n) : wordOfSupport (wordSupport x) = x

theorem MetricCodes.wordOfSupport_injective {n : ℕ} : Function.Injective wordOfSupport

theorem MetricCodes.binaryWeight_eq_card_wordSupport {n : ℕ} (x : BinaryWord n) : binaryWeight x = (wordSupport x).card

theorem MetricCodes.hammingDist_comm {n : ℕ} (x y : BinaryWord n) : hammingDist x y = hammingDist y x

theorem MetricCodes.hammingDist_eq_card_support_sdiff {n : ℕ} (x y : BinaryWord n) : hammingDist x y = (wordSupport x \ wordSupport y).card + (wordSupport y \ wordSupport x).card

theorem MetricCodes.hammingDist_eq_two_mul_of_binaryWeight_eq {n : ℕ} (x y : BinaryWord n) (hweight : binaryWeight x = binaryWeight y) : hammingDist x y = 2 * (wordSupport x \ wordSupport y).card

def MetricCodes.johnsonDist {n w : ℕ} (x y : JohnsonSphere n w) : ℕ

The johnson dist used in the metric-code argument.

Equations

• MetricCodes.johnsonDist x y = (MetricCodes.wordSupport ↑x \ MetricCodes.wordSupport ↑y).card

theorem MetricCodes.hammingDist_eq_two_mul_johnsonDist {n w : ℕ} (x y : JohnsonSphere n w) : hammingDist ↑x ↑y = 2 * johnsonDist x y

theorem MetricCodes.johnsonDist_eq_weight_sub_inter {n w : ℕ} (x y : JohnsonSphere n w) : johnsonDist x y = w - (wordSupport ↑x ∩ wordSupport ↑y).card

def MetricCodes.binaryTranslate {n : ℕ} (x y : BinaryWord n) : BinaryWord n

Translate a binary word by coordinatewise exclusive-or with x.

Equations

• MetricCodes.binaryTranslate x y i = (x i ^^ y i)

@[simp]

theorem MetricCodes.binaryTranslate_involutive {n : ℕ} (x y : BinaryWord n) : binaryTranslate x (binaryTranslate x y) = y

theorem MetricCodes.binaryTranslate_injective {n : ℕ} (x : BinaryWord n) : Function.Injective (binaryTranslate x)

theorem MetricCodes.hammingDist_binaryTranslate {n : ℕ} (z x y : BinaryWord n) : hammingDist (binaryTranslate z x) (binaryTranslate z y) = hammingDist x y

theorem MetricCodes.binaryWeight_binaryTranslate {n : ℕ} (x y : BinaryWord n) : binaryWeight (binaryTranslate x y) = hammingDist x y

def MetricCodes.weightShell (n w : ℕ) : Finset (BinaryWord n)

The finite set of length-n binary words of weight w.

Equations

• MetricCodes.weightShell n w = {x : MetricCodes.BinaryWord n | MetricCodes.binaryWeight x = w}

@[simp]

theorem MetricCodes.mem_weightShell {n w : ℕ} (x : BinaryWord n) : x ∈ weightShell n w ↔ binaryWeight x = w

theorem MetricCodes.weightShell_eq_image (n w : ℕ) : weightShell n w = Finset.image wordOfSupport (Finset.powersetCard w Finset.univ)

theorem MetricCodes.card_weightShell (n w : ℕ) : (weightShell n w).card = n.choose w

def MetricCodes.hammingSphere {n : ℕ} (x : BinaryWord n) (r : ℕ) : Finset (BinaryWord n)

The finite set of binary words at Hamming distance exactly r from x.

Equations

• MetricCodes.hammingSphere x r = {y : MetricCodes.BinaryWord n | MetricCodes.hammingDist x y = r}

@[simp]

theorem MetricCodes.mem_hammingSphere {n r : ℕ} (x y : BinaryWord n) : y ∈ hammingSphere x r ↔ hammingDist x y = r

theorem MetricCodes.hammingSphere_eq_image {n : ℕ} (x : BinaryWord n) (r : ℕ) : hammingSphere x r = Finset.image (binaryTranslate x) (weightShell n r)

theorem MetricCodes.card_hammingSphere {n : ℕ} (x : BinaryWord n) (r : ℕ) : (hammingSphere x r).card = n.choose r

def MetricCodes.localizedCode {n : ℕ} (C : Finset (BinaryWord n)) (z : BinaryWord n) (w : ℕ) : Finset (BinaryWord n)

The words of C whose translate by z has weight w.

Equations

• MetricCodes.localizedCode C z w = {x ∈ C | MetricCodes.binaryWeight (MetricCodes.binaryTranslate z x) = w}

@[simp]

theorem MetricCodes.mem_localizedCode {n w : ℕ} (C : Finset (BinaryWord n)) (z x : BinaryWord n) : x ∈ localizedCode C z w ↔ x ∈ C ∧ binaryWeight (binaryTranslate z x) = w

def MetricCodes.translateLocalizedCode {n : ℕ} (C : Finset (BinaryWord n)) (z : BinaryWord n) (w : ℕ) : Finset (BinaryWord n)

Translate the localized code by z into the weight-w shell.

Equations

• MetricCodes.translateLocalizedCode C z w = Finset.image (MetricCodes.binaryTranslate z) (MetricCodes.localizedCode C z w)

theorem MetricCodes.translateLocalizedCode_subset_weightShell {n w : ℕ} (C : Finset (BinaryWord n)) (z : BinaryWord n) : translateLocalizedCode C z w ⊆ weightShell n w

theorem MetricCodes.card_translateLocalizedCode {n w : ℕ} (C : Finset (BinaryWord n)) (z : BinaryWord n) : (translateLocalizedCode C z w).card = (localizedCode C z w).card

theorem MetricCodes.translateLocalizedCode_isBinaryCode {n d w : ℕ} (C : Finset (BinaryWord n)) (z : BinaryWord n) (hC : IsBinaryCode d C) : IsBinaryCode d (translateLocalizedCode C z w)

theorem MetricCodes.localization_double_count {n : ℕ} (C : Finset (BinaryWord n)) (w : ℕ) : ∑ z : BinaryWord n, (localizedCode C z w).card = C.card * n.choose w

theorem MetricCodes.bassalygo_elias_bound {n d w B : ℕ} (C : Finset (BinaryWord n)) (hC : IsBinaryCode d C) (hB : ∀ D ⊆ weightShell n w, IsBinaryCode d D → D.card ≤ B) : C.card * n.choose w ≤ 2 ^ n * B

def MetricCodes.precedingBinomial (n : ℕ) : ℕ → ℕ

The preceding binomial used in the metric-code argument.

Equations

• MetricCodes.precedingBinomial n 0 = 0
• MetricCodes.precedingBinomial n k.succ = n.choose k

theorem MetricCodes.choose_monotone_to_half (n : ℕ) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ n / 2) : n.choose i ≤ n.choose j

def MetricCodes.johnsonAmbientDimension (n a L : ℕ) : ℕ

The johnson ambient dimension used in the metric-code argument.

Equations

• MetricCodes.johnsonAmbientDimension n a L = ∑ j ∈ Finset.Icc a L, MetricCodes.booleanHarmonicDimension n j

theorem MetricCodes.johnsonAmbientDimension_eq (n a L : ℕ) (haL : a ≤ L) (hL : L ≤ n / 2) : johnsonAmbientDimension n a L = n.choose L - precedingBinomial n a

theorem MetricCodes.johnsonAmbientDimension_eq_of_fibre (n p q L : ℕ) (hpq : p + q ≤ L) (hL : L ≤ n / 2) : johnsonAmbientDimension n (p + q) L = n.choose L - precedingBinomial n (p + q)

@[reducible, inline]

abbrev SpherePacking.Euclidean (n : ℕ) : Type

The euclidean used in the spherical-code argument.

Equations

• SpherePacking.Euclidean n = EuclideanSpace ℝ (Fin n)

noncomputable def SpherePacking.factorialLogError (n : ℕ) : ℝ

The error in the normalized factorial-log approximation log (n!) / n = log n - 1.

Equations

• SpherePacking.factorialLogError n = Real.log ↑n.factorial / ↑n - Real.log ↑n + 1

theorem SpherePacking.tendsto_log_natCast_div_natCast : Filter.Tendsto (fun (n : ℕ) => Real.log ↑n / ↑n) Filter.atTop (nhds 0)

theorem SpherePacking.tendsto_log_two_mul_natCast_div_natCast : Filter.Tendsto (fun (n : ℕ) => Real.log (2 * ↑n) / ↑n) Filter.atTop (nhds 0)

theorem SpherePacking.tendsto_log_stirlingSeq_div_natCast : Filter.Tendsto (fun (n : ℕ) => Real.log (Stirling.stirlingSeq n) / ↑n) Filter.atTop (nhds 0)

theorem SpherePacking.factorialLogError_eq (n : ℕ) (hn : n ≠ 0) : factorialLogError n = Real.log (Stirling.stirlingSeq n) / ↑n + 1 / 2 * Real.log (2 * ↑n) / ↑n

theorem SpherePacking.tendsto_factorialLogError : Filter.Tendsto factorialLogError Filter.atTop (nhds 0)

theorem SpherePacking.scaled_log_factorial_identity (m n : ℕ) (hm : m ≠ 0) (hn : n ≠ 0) : Real.log ↑m.factorial / ↑n - ↑m / ↑n * Real.log ↑n = ↑m / ↑n * (factorialLogError m + Real.log (↑m / ↑n) - 1)

theorem SpherePacking.tendsto_scaled_log_factorial_sub (k : ℕ → ℕ) (u : ℝ) (hk : Filter.Tendsto k Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds u)) (hu : u ≠ 0) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(k n).factorial / ↑n - ↑(k n) / ↑n * Real.log ↑n) Filter.atTop (nhds (u * Real.log u - u))

theorem SpherePacking.log_add_choose_div_eq (a b n : ℕ) : Real.log ↑((a + b).choose a) / ↑n = Real.log ↑(a + b).factorial / ↑n - Real.log ↑a.factorial / ↑n - Real.log ↑b.factorial / ↑n

theorem SpherePacking.tendsto_log_add_choose_div (k l : ℕ → ℕ) (u v : ℝ) (hk : Filter.Tendsto k Filter.atTop Filter.atTop) (hl : Filter.Tendsto l Filter.atTop Filter.atTop) (hku : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds u)) (hlv : Filter.Tendsto (fun (n : ℕ) => ↑(l n) / ↑n) Filter.atTop (nhds v)) (hu : 0 < u) (hv : 0 < v) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑((k n + l n).choose (k n)) / ↑n) Filter.atTop (nhds ((u + v) * Real.log (u + v) - u * Real.log u - v * Real.log v))

noncomputable def MetricCodes.Hamming.validCodes (n d : ℕ) : Finset (Finset (BinaryWord n))

The finite family of length-n binary codes with minimum distance at least d.

Equations

• MetricCodes.Hamming.validCodes n d = Finset.filter (MetricCodes.IsBinaryCode d) Finset.univ

theorem MetricCodes.Hamming.mem_validCodes {n d : ℕ} (C : Finset (BinaryWord n)) : C ∈ validCodes n d ↔ IsBinaryCode d C

theorem MetricCodes.Hamming.validCodes_nonempty (n d : ℕ) : (validCodes n d).Nonempty

noncomputable def MetricCodes.Hamming.codeNumber (n d : ℕ) : ℕ

The code number used in the binary-code argument.

Equations

• MetricCodes.Hamming.codeNumber n d = (MetricCodes.Hamming.validCodes n d).sup fun (C : Finset (MetricCodes.BinaryWord n)) => C.card

theorem MetricCodes.Hamming.card_le_codeNumber {n d : ℕ} (C : Finset (BinaryWord n)) (hC : IsBinaryCode d C) : C.card ≤ codeNumber n d

theorem MetricCodes.Hamming.exists_codeNumber (n d : ℕ) : ∃ (C : Finset (BinaryWord n)), IsBinaryCode d C ∧ C.card = codeNumber n d

theorem MetricCodes.Hamming.codeNumber_real_le_of_forall {n d : ℕ} {B : ℝ} (h : ∀ (C : Finset (BinaryWord n)), IsBinaryCode d C → ↑C.card ≤ B) : ↑(codeNumber n d) ≤ B

theorem MetricCodes.Hamming.codeNumber_pos (n d : ℕ) : 0 < codeNumber n d

def MetricCodes.Hamming.ambientDimension (n k L : ℕ) : ℕ

The ambient dimension used in the binary-code argument.

Equations

• MetricCodes.Hamming.ambientDimension n k L = ∑ j ∈ Finset.range (L - k + 1), n.choose (k + j)

theorem MetricCodes.Hamming.hammingFibreDimension_pos {n k : ℕ} (hk : 2 * k ≤ n) : 0 < hammingFibreDimension n k

noncomputable def MetricCodes.Hamming.threshold (n d : ℕ) : ℝ

The threshold used in the binary-code argument.

Equations

• MetricCodes.Hamming.threshold n d = 1 - 2 * ↑d / ↑n

theorem MetricCodes.Hamming.threshold_lt_one {n d : ℕ} (hn : 0 < n) (hd : 0 < d) : threshold n d < 1

@[reducible, inline]

abbrev MetricCodes.Hamming.Index (k L : ℕ) : Type

The index used in the binary-code argument.

Equations

• MetricCodes.Hamming.Index k L = Fin (L - k + 1)

@[reducible, inline]

abbrev MetricCodes.Hamming.Space (k L : ℕ) : Type

The space used in the binary-code argument.

Equations

• MetricCodes.Hamming.Space k L = EuclideanSpace ℝ (MetricCodes.Hamming.Index k L)

noncomputable def MetricCodes.Hamming.matrix (n k L : ℕ) : Matrix (Index k L) (Index k L) ℝ

The matrix used in the binary-code argument.

Equations

• MetricCodes.Hamming.matrix n k L = MetricCodes.hammingJacobiMatrix n k L

theorem MetricCodes.Hamming.matrix_hermitian (n k L : ℕ) : (matrix n k L).IsHermitian

noncomputable def MetricCodes.Hamming.operator (n k L : ℕ) : Space k L →ₗ[ℝ] Space k L

The operator used in the binary-code argument.

Equations

• MetricCodes.Hamming.operator n k L = Matrix.toEuclideanLin (MetricCodes.Hamming.matrix n k L)

theorem MetricCodes.Hamming.operator_isSymmetric (n k L : ℕ) : (operator n k L).IsSymmetric

noncomputable def MetricCodes.Hamming.continuousOperator (n k L : ℕ) : Space k L →L[ℝ] Space k L

The continuous operator used in the binary-code argument.

Equations

• MetricCodes.Hamming.continuousOperator n k L = LinearMap.toContinuousLinearMap (MetricCodes.Hamming.operator n k L)

noncomputable def MetricCodes.Hamming.rayleigh (n k L : ℕ) (x : Space k L) : ℝ

The rayleigh used in the binary-code argument.

Equations

• MetricCodes.Hamming.rayleigh n k L x = (MetricCodes.Hamming.continuousOperator n k L).rayleighQuotient x

theorem MetricCodes.Hamming.rayleigh_bddAbove (n k L : ℕ) : BddAbove (Set.range fun (x : { x : Space k L // x ≠ 0 }) => rayleigh n k L ↑x)

noncomputable def MetricCodes.Hamming.topEigenvalue (n k L : ℕ) : ℝ

The top eigenvalue used in the binary-code argument.

Equations

• MetricCodes.Hamming.topEigenvalue n k L = ⨆ (x : { x : MetricCodes.Hamming.Space k L // x ≠ 0 }), MetricCodes.Hamming.rayleigh n k L ↑x

theorem MetricCodes.Hamming.rayleigh_le_top (n k L : ℕ) (x : Space k L) (hx : x ≠ 0) : rayleigh n k L x ≤ topEigenvalue n k L

theorem MetricCodes.Hamming.topEigenvalue_hasEigenvalue (n k L : ℕ) : Module.End.HasEigenvalue (operator n k L) (topEigenvalue n k L)

theorem MetricCodes.Hamming.exists_topEigenvector (n k L : ℕ) : ∃ (x : Space k L), x ≠ 0 ∧ (operator n k L) x = topEigenvalue n k L • x

theorem MetricCodes.Hamming.rayleigh_eq_inner (n k L : ℕ) (x : Space k L) : rayleigh n k L x = inner ℝ ((operator n k L) x) x / ‖x‖ ^ 2

@[reducible, inline]

abbrev MetricCodes.Hamming.coordinateAbs (k L : ℕ) (x : Space k L) : Space k L

The coordinate abs used in the binary-code argument.

Equations

• MetricCodes.Hamming.coordinateAbs k L x = MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs x

theorem MetricCodes.Hamming.coordinateAbs_nonneg (k L : ℕ) (x : Space k L) (p : Index k L) : 0 ≤ (coordinateAbs k L x).ofLp p

theorem MetricCodes.Hamming.coordinateAbs_norm (k L : ℕ) (x : Space k L) : ‖coordinateAbs k L x‖ = ‖x‖

theorem MetricCodes.Hamming.coordinateAbs_ne_zero (k L : ℕ) {x : Space k L} (hx : x ≠ 0) : coordinateAbs k L x ≠ 0

theorem MetricCodes.Hamming.matrix_entry_nonneg {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (p q : Index k L) : 0 ≤ matrix n k L p q

theorem MetricCodes.Hamming.inner_le_inner_coordinateAbs {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (x : Space k L) : inner ℝ ((operator n k L) x) x ≤ inner ℝ ((operator n k L) (coordinateAbs k L x)) (coordinateAbs k L x)

theorem MetricCodes.Hamming.rayleigh_le_coordinateAbs {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (x : Space k L) : rayleigh n k L x ≤ rayleigh n k L (coordinateAbs k L x)

theorem MetricCodes.Hamming.rayleigh_eq_of_eigenvector (n k L : ℕ) (x : Space k L) (hx : x ≠ 0) (eigenvalue : ℝ) (heig : (operator n k L) x = eigenvalue • x) : rayleigh n k L x = eigenvalue

theorem MetricCodes.Hamming.coordinateAbs_top_rayleigh {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (x : Space k L) (hx : x ≠ 0) (heig : (operator n k L) x = topEigenvalue n k L • x) : rayleigh n k L (coordinateAbs k L x) = topEigenvalue n k L

theorem MetricCodes.Hamming.exists_nonnegative_topEigenvector {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) : ∃ (x : Space k L), x ≠ 0 ∧ (operator n k L) x = topEigenvalue n k L • x ∧ ∀ (p : Index k L), 0 ≤ x.ofLp p

theorem MetricCodes.Hamming.exists_nonnegative_unit_topEigenvector {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) : ∃ (x : Space k L), ‖x‖ = 1 ∧ (operator n k L) x = topEigenvalue n k L • x ∧ ∀ (p : Index k L), 0 ≤ x.ofLp p

theorem MetricCodes.Hamming.matrix_adjacent_pos {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (p q : Index k L) (hadjacent : ↑p + 1 = ↑q ∨ ↑q + 1 = ↑p) : 0 < matrix n k L p q

theorem MetricCodes.Hamming.nonnegative_eigenvector_zero_propagates {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : Space k L) (eigenvalue : ℝ) (heigen : (operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Index k L), 0 ≤ v.ofLp i) (p q : Index k L) (hp : v.ofLp p = 0) (hadjacent : ↑p + 1 = ↑q ∨ ↑q + 1 = ↑p) : v.ofLp q = 0

theorem MetricCodes.Hamming.nonnegative_eigenvector_coordinate_pos {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) (v : Space k L) (eigenvalue : ℝ) (heigen : (operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Index k L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) (i : Index k L) : 0 < v.ofLp i

theorem MetricCodes.Hamming.nonnegative_eigenvalue_pos_of_lt {n k L : ℕ} (hn : 0 < n) (hkL : k < L) (hLn : L + k ≤ n) (v : Space k L) (eigenvalue : ℝ) (heigen : (operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Index k L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) : 0 < eigenvalue

theorem MetricCodes.Hamming.exists_positive_unit_topEigenvector {n k L : ℕ} (hn : 0 < n) (hkL : k ≤ L) (hLn : L + k ≤ n) : ∃ (v : Space k L), ‖v‖ = 1 ∧ (operator n k L) v = topEigenvalue n k L • v ∧ ∀ (i : Index k L), 0 < v.ofLp i

theorem MetricCodes.Hamming.topEigenvalue_pos {n k L : ℕ} (hn : 0 < n) (hkL : k < L) (hLn : L + k ≤ n) : 0 < topEigenvalue n k L

theorem MetricCodes.Hamming.finite_bound_of_projection_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n k L d : ℕ} (hn : 0 < n) (hd : 0 < d) (C : Finset (BinaryWord n)) (hC : IsBinaryCode d C) (P : ProjectionFamily (BinaryWord n) (ambientDimension n k L) (hammingFibreDimension n k)) (q : BinaryWord n → E) (hrank : 0 < hammingFibreDimension n k) (hgap : threshold n d < topEigenvalue n k L) (hgram : ∀ x ∈ C, ∀ y ∈ C, inner ℝ (q x) (q y) = (hammingCorrelation x y - topEigenvalue n k L) * P.overlap x y) : ↑C.card ≤ (1 - threshold n d) / (topEigenvalue n k L - threshold n d) * (↑(ambientDimension n k L) / ↑(hammingFibreDimension n k))

theorem MetricCodes.Hamming.finite_codeNumber_bound_of_projection_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n k L d : ℕ} (hn : 0 < n) (hd : 0 < d) (P : ProjectionFamily (BinaryWord n) (ambientDimension n k L) (hammingFibreDimension n k)) (q : BinaryWord n → E) (hrank : 0 < hammingFibreDimension n k) (hgap : threshold n d < topEigenvalue n k L) (hgram : ∀ (x y : BinaryWord n), inner ℝ (q x) (q y) = (hammingCorrelation x y - topEigenvalue n k L) * P.overlap x y) : ↑(codeNumber n d) ≤ (1 - threshold n d) / (topEigenvalue n k L - threshold n d) * (↑(ambientDimension n k L) / ↑(hammingFibreDimension n k))

theorem MetricCodes.Hamming.binaryEntropy_eq_binEntropy_div_log (u : ℝ) : binaryEntropy u = Real.binEntropy u / Real.log 2

theorem MetricCodes.Hamming.binaryEntropy_le_one (u : ℝ) : binaryEntropy u ≤ 1

theorem MetricCodes.Hamming.binaryEntropy_continuous : Continuous binaryEntropy

def MetricCodes.Hamming.Feasible (δ a b : ℝ) : Prop

The feasible used in the binary-code argument.

Equations

• MetricCodes.Hamming.Feasible δ a b = (0 ≤ b ∧ b < a ∧ a ≤ 1 / 2 ∧ 1 - 2 * δ < MetricCodes.hammingGamma a b)

def MetricCodes.Hamming.rateSet (δ : ℝ) : Set ℝ

The rate set used in the binary-code argument.

Equations

• MetricCodes.Hamming.rateSet δ = {r : ℝ | ∃ (a : ℝ) (b : ℝ), MetricCodes.Hamming.Feasible δ a b ∧ r = MetricCodes.binaryEntropy a - MetricCodes.binaryEntropy b}

noncomputable def MetricCodes.Hamming.variationalRate (δ : ℝ) : ℝ

The variational rate used in the binary-code argument.

Equations

• MetricCodes.Hamming.variationalRate δ = sInf (MetricCodes.Hamming.rateSet δ)

theorem MetricCodes.Hamming.rateSet_bddBelow (δ : ℝ) : BddBelow (rateSet δ)

theorem MetricCodes.Hamming.variationalRate_le_of_feasible {δ a b : ℝ} (h : Feasible δ a b) : variationalRate δ ≤ binaryEntropy a - binaryEntropy b

noncomputable def MetricCodes.Hamming.classicalParameter (δ : ℝ) : ℝ

The classical parameter used in the binary-code argument.

Equations

• MetricCodes.Hamming.classicalParameter δ = 1 / 2 - √(δ * (1 - δ))

noncomputable def MetricCodes.Hamming.classicalRate (δ : ℝ) : ℝ

The classical rate used in the binary-code argument.

Equations

• MetricCodes.Hamming.classicalRate δ = MetricCodes.binaryEntropy (MetricCodes.Hamming.classicalParameter δ)

theorem MetricCodes.Hamming.classicalParameter_lt_half {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : classicalParameter δ < 1 / 2

theorem MetricCodes.Hamming.classicalParameter_pos {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : 0 < classicalParameter δ

theorem MetricCodes.Hamming.classicalParameter_mul_one_sub {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : classicalParameter δ * (1 - classicalParameter δ) = (1 / 2 - δ) ^ 2

theorem MetricCodes.Hamming.hammingGamma_zero {a : ℝ} (ha : 0 < a) (ha' : a < 1) : hammingGamma a 0 = 2 * √(a * (1 - a))

theorem MetricCodes.Hamming.hammingGamma_classicalParameter {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : hammingGamma (classicalParameter δ) 0 = 1 - 2 * δ

noncomputable def MetricCodes.Hamming.improvementSlope (a : ℝ) : ℝ

The slope 2 / (1 - 2 * a) + 1 used to perturb the Hamming bound parameters.

Equations

• MetricCodes.Hamming.improvementSlope a = 2 / (1 - 2 * a) + 1

noncomputable def MetricCodes.Hamming.improvementPath (a b : ℝ) : ℝ

The affine perturbation of a with slope improvementSlope a and parameter b.

Equations

• MetricCodes.Hamming.improvementPath a b = a + MetricCodes.Hamming.improvementSlope a * b

theorem MetricCodes.Hamming.improvementSlope_gt_one {a : ℝ} (ha : a < 1 / 2) : 1 < improvementSlope a

theorem MetricCodes.Hamming.tendsto_improvementPath_zero (a : ℝ) : Filter.Tendsto (improvementPath a) (nhdsWithin 0 (Set.Ioi 0)) (nhds a)

def MetricCodes.Hamming.spectralMarginPolynomial (a c b : ℝ) : ℝ

The cubic factor remaining after extracting b from the difference of the squared spectral- bound expressions.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Hamming.spectralMarginPolynomial_factor (a c b : ℝ) : ((a + c * b - b) * (1 - (a + c * b) - b)) ^ 2 - a * (1 - a) * ((a + c * b) * (1 - (a + c * b))) = b * spectralMarginPolynomial a c b

theorem MetricCodes.Hamming.spectralMarginPolynomial_continuous (a c : ℝ) : Continuous (spectralMarginPolynomial a c)

theorem MetricCodes.Hamming.spectralMarginPolynomial_improvement_zero {a : ℝ} (ha : a < 1 / 2) : spectralMarginPolynomial a (improvementSlope a) 0 = a * (1 - a) * (1 - 2 * a)

theorem MetricCodes.Hamming.eventually_hammingGamma_improvement {a : ℝ} (ha : 0 < a) (ha' : a < 1 / 2) : ∀ᶠ (b : ℝ) in nhdsWithin 0 (Set.Ioi 0), hammingGamma a 0 < hammingGamma (improvementPath a b) b

theorem MetricCodes.Hamming.differentiableAt_binaryEntropy {a : ℝ} (ha : 0 < a) (ha' : a < 1) : DifferentiableAt ℝ binaryEntropy a

theorem MetricCodes.Hamming.neg_mul_logb_le_binaryEntropy {b : ℝ} (hb : 0 ≤ b) (hb' : b ≤ 1) : b * -Real.logb 2 b ≤ binaryEntropy b

theorem MetricCodes.Hamming.eventually_binaryEntropy_improvement {a : ℝ} (ha : 0 < a) (ha' : a < 1 / 2) : ∀ᶠ (b : ℝ) in nhdsWithin 0 (Set.Ioi 0), binaryEntropy (improvementPath a b) - binaryEntropy b < binaryEntropy a

theorem MetricCodes.Hamming.exists_strict_improving_feasible {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : ∃ (a : ℝ) (b : ℝ), Feasible δ a b ∧ binaryEntropy a - binaryEntropy b < classicalRate δ

theorem MetricCodes.Hamming.variationalRate_lt_classicalRate {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : variationalRate δ < classicalRate δ

noncomputable def MetricCodes.Hamming.longitudinalDegree (a : ℝ) (n : ℕ) : ℕ

The longitudinal degree used in the binary-code argument.

Equations

• MetricCodes.Hamming.longitudinalDegree a n = ⌊a * ↑n⌋₊

noncomputable def MetricCodes.Hamming.transverseDegree (b : ℝ) (n : ℕ) : ℕ

The transverse degree used in the binary-code argument.

Equations

• MetricCodes.Hamming.transverseDegree b n = ⌊b * ↑n⌋₊

theorem MetricCodes.Hamming.tendsto_longitudinal_ratio {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => ↑(longitudinalDegree a n) / ↑n) Filter.atTop (nhds a)

theorem MetricCodes.Hamming.tendsto_transverse_ratio {b : ℝ} (hb : 0 ≤ b) : Filter.Tendsto (fun (n : ℕ) => ↑(transverseDegree b n) / ↑n) Filter.atTop (nhds b)

theorem MetricCodes.Hamming.tendsto_terminal_degree_ratio {a : ℝ} (ha : 0 < a) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(longitudinalDegree a n - r) / ↑n) Filter.atTop (nhds a)

noncomputable def MetricCodes.Hamming.normalizedCoefficient (x y z : ℝ) : ℝ

The normalized coefficient used in the binary-code argument.

Equations

• MetricCodes.Hamming.normalizedCoefficient x y z = (x - y + z) * (1 - x - y) / √((x + z) * (1 - x))

theorem MetricCodes.Hamming.hammingJacobiEntry_eq_normalized (n k i : ℕ) (hn : 0 < n) : hammingJacobiEntry n k i = normalizedCoefficient (↑i / ↑n) (↑k / ↑n) (1 / ↑n)

theorem MetricCodes.Hamming.normalizedCoefficient_zero (a b : ℝ) : normalizedCoefficient a b 0 = hammingGamma a b / 2

theorem MetricCodes.Hamming.tendsto_terminal_coefficient {a b : ℝ} (ha : 0 < a) (ha' : a < 1) (hb : 0 ≤ b) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => hammingJacobiEntry n (transverseDegree b n) (longitudinalDegree a n - r)) Filter.atTop (nhds (hammingGamma a b / 2))

theorem MetricCodes.Hamming.tridiagonal_quadratic_sum (d : ℕ) (c v : ℕ → ℝ) : ∑ p ∈ Finset.range (d + 1), ∑ q ∈ Finset.range (d + 1), (if p + 1 = q then c p else if q + 1 = p then c q else 0) * v q * v p = 2 * ∑ p ∈ Finset.range d, c p * v p * v (p + 1)

def MetricCodes.Hamming.terminalIndicator (d m p : ℕ) : ℝ

The terminal indicator used in the binary-code argument.

Equations

• MetricCodes.Hamming.terminalIndicator d m p = if d - m ≤ p then 1 else 0

theorem MetricCodes.Hamming.terminal_indicator_sum (d m : ℕ) (hm : m ≤ d) : ∑ p ∈ Finset.range (d + 1), terminalIndicator d m p = ↑m + 1

theorem MetricCodes.Hamming.terminal_indicator_edge_sum (d m : ℕ) (hm : m ≤ d) (c : ℕ → ℝ) : ∑ p ∈ Finset.range d, c p * terminalIndicator d m p * terminalIndicator d m (p + 1) = ∑ r ∈ Finset.range m, c (d - m + r)

def MetricCodes.Hamming.terminalVector (k L m : ℕ) : Space k L

The terminal vector used in the binary-code argument.

Equations

• MetricCodes.Hamming.terminalVector k L m = WithLp.toLp 2 fun (p : Fin (L - k + 1)) => MetricCodes.Hamming.terminalIndicator (L - k) m ↑p

theorem MetricCodes.Hamming.terminalVector_last (k L m : ℕ) : (terminalVector k L m).ofLp (Fin.last (L - k)) = 1

theorem MetricCodes.Hamming.terminalVector_ne_zero (k L m : ℕ) : terminalVector k L m ≠ 0

theorem MetricCodes.Hamming.terminalVector_norm_sq (k L m : ℕ) (hm : m ≤ L - k) : ‖terminalVector k L m‖ ^ 2 = ↑m + 1

theorem MetricCodes.Hamming.terminalVector_inner (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : inner ℝ ((operator n k L) (terminalVector k L m)) (terminalVector k L m) = 2 * ∑ r ∈ Finset.range m, hammingJacobiEntry n k (L - m + r)

theorem MetricCodes.Hamming.terminalVector_rayleigh (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : rayleigh n k L (terminalVector k L m) = (2 * ∑ r ∈ Finset.range m, hammingJacobiEntry n k (L - m + r)) / (↑m + 1)

theorem MetricCodes.Hamming.terminal_edge_sum_le_top (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : (2 * ∑ r ∈ Finset.range m, hammingJacobiEntry n k (L - m + r)) / (↑m + 1) ≤ topEigenvalue n k L

theorem MetricCodes.Hamming.eventually_transverse_add_le_longitudinal {a b : ℝ} (hb : 0 ≤ b) (hba : b < a) (m : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, transverseDegree b n + m ≤ longitudinalDegree a n

noncomputable def MetricCodes.Hamming.terminalEdgeRayleigh (a b : ℝ) (m n : ℕ) : ℝ

The terminal edge rayleigh used in the binary-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Hamming.tendsto_terminalEdgeRayleigh {a b : ℝ} (ha : 0 < a) (ha' : a < 1) (hb : 0 ≤ b) (m : ℕ) : Filter.Tendsto (terminalEdgeRayleigh a b m) Filter.atTop (nhds (↑m / (↑m + 1) * hammingGamma a b))

theorem MetricCodes.Hamming.terminalEdgeRayleigh_le_top (a b : ℝ) (m n : ℕ) (hfit : transverseDegree b n + m ≤ longitudinalDegree a n) : terminalEdgeRayleigh a b m n ≤ topEigenvalue n (transverseDegree b n) (longitudinalDegree a n)

theorem MetricCodes.Hamming.eventually_topEigenvalue_gt {a b s : ℝ} (hb : 0 ≤ b) (hba : b < a) (ha : a ≤ 1 / 2) (hs : s < hammingGamma a b) : ∀ᶠ (n : ℕ) in Filter.atTop, s < topEigenvalue n (transverseDegree b n) (longitudinalDegree a n)

theorem MetricCodes.Hamming.longitudinalDegree_le_dimension {a : ℝ} (ha : a ≤ 1) (n : ℕ) : longitudinalDegree a n ≤ n

theorem MetricCodes.Hamming.complement_longitudinalDegree_floor_le {a : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) (n : ℕ) : longitudinalDegree (1 - a) n ≤ n - longitudinalDegree a n

theorem MetricCodes.Hamming.tendsto_complement_longitudinalDegree {a : ℝ} (ha : 0 ≤ a) (ha' : a < 1) : Filter.Tendsto (fun (n : ℕ) => n - longitudinalDegree a n) Filter.atTop Filter.atTop

theorem MetricCodes.Hamming.tendsto_complement_longitudinal_ratio {a : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(n - longitudinalDegree a n) / ↑n) Filter.atTop (nhds (1 - a))

theorem MetricCodes.Hamming.tendsto_log_choose_longitudinal {a : ℝ} (ha : 0 < a) (ha' : a < 1) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(n.choose (longitudinalDegree a n)) / ↑n) Filter.atTop (nhds (Real.binEntropy a))

theorem MetricCodes.Hamming.tendsto_logb_choose_longitudinal {a : ℝ} (ha : 0 < a) (ha' : a < 1) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(n.choose (longitudinalDegree a n)) / ↑n) Filter.atTop (nhds (binaryEntropy a))

theorem MetricCodes.Hamming.longitudinalDegree_le_half {a : ℝ} (ha : a ≤ 1 / 2) (n : ℕ) : longitudinalDegree a n ≤ n / 2

theorem MetricCodes.Hamming.choose_le_ambientDimension (n k L : ℕ) (hkL : k ≤ L) : n.choose L ≤ ambientDimension n k L

theorem MetricCodes.Hamming.ambientDimension_le_mul_choose (n k L : ℕ) (hkL : k ≤ L) (hL : L ≤ n / 2) : ambientDimension n k L ≤ (n + 1) * n.choose L

theorem MetricCodes.Hamming.choose_le_mul_hammingFibreDimension {n k : ℕ} (hk : 2 * k ≤ n) : n.choose k ≤ (n + 1) * hammingFibreDimension n k

theorem MetricCodes.Hamming.hammingFibreDimension_le_choose (n k : ℕ) : hammingFibreDimension n k ≤ n.choose k

theorem MetricCodes.Hamming.tendsto_logb_succ_div : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(n + 1) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Hamming.tendsto_logb_ambientDimension {a b : ℝ} (hb : 0 ≤ b) (hba : b < a) (ha : a ≤ 1 / 2) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(ambientDimension n (transverseDegree b n) (longitudinalDegree a n)) / ↑n) Filter.atTop (nhds (binaryEntropy a))

theorem MetricCodes.Hamming.tendsto_logb_hammingFibreDimension {b : ℝ} (hb : 0 < b) (hb' : b ≤ 1 / 2) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(hammingFibreDimension n (transverseDegree b n)) / ↑n) Filter.atTop (nhds (binaryEntropy b))

noncomputable def MetricCodes.Hamming.binaryRate (δ : ℝ) : ℝ

The binary rate used in the binary-code argument.

Equations

• MetricCodes.Hamming.binaryRate δ = Filter.limsup (fun (n : ℕ) => Real.logb 2 ↑(MetricCodes.Hamming.codeNumber n ⌈δ * ↑n⌉₊) / ↑n) Filter.atTop

theorem MetricCodes.Hamming.tendsto_ceil_distance_ratio {δ : ℝ} (hδ : 0 ≤ δ) : Filter.Tendsto (fun (n : ℕ) => ↑⌈δ * ↑n⌉₊ / ↑n) Filter.atTop (nhds δ)

theorem MetricCodes.Hamming.tendsto_threshold_ceil {δ : ℝ} (hδ : 0 ≤ δ) : Filter.Tendsto (fun (n : ℕ) => threshold n ⌈δ * ↑n⌉₊) Filter.atTop (nhds (1 - 2 * δ))

theorem MetricCodes.Hamming.ceil_distance_pos {δ : ℝ} (hδ : 0 < δ) {n : ℕ} (hn : 0 < n) : 0 < ⌈δ * ↑n⌉₊

noncomputable def MetricCodes.Hamming.windowFibreQuotient (a b : ℝ) (n : ℕ) : ℝ

The window fibre quotient used in the binary-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Hamming.windowFibreQuotient_pos_of_fit {a b : ℝ} {n : ℕ} (ha : a ≤ 1 / 2) (hfit : transverseDegree b n ≤ longitudinalDegree a n) : 0 < windowFibreQuotient a b n

theorem MetricCodes.Hamming.eventually_windowFibreQuotient_pos {a b : ℝ} (hb : 0 ≤ b) (hba : b < a) (ha : a ≤ 1 / 2) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < windowFibreQuotient a b n

theorem MetricCodes.Hamming.tendsto_logb_windowFibreQuotient {a b : ℝ} (hb : 0 < b) (hba : b < a) (ha : a ≤ 1 / 2) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (windowFibreQuotient a b n) / ↑n) Filter.atTop (nhds (binaryEntropy a - binaryEntropy b))

theorem MetricCodes.Hamming.tendsto_logb_const_mul_windowFibreQuotient {a b C : ℝ} (hb : 0 < b) (hba : b < a) (ha : a ≤ 1 / 2) (hC : 0 < C) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (C * windowFibreQuotient a b n) / ↑n) Filter.atTop (nhds (binaryEntropy a - binaryEntropy b))

theorem MetricCodes.Hamming.codeLogRate_nonneg (δ : ℝ) (n : ℕ) : 0 ≤ Real.logb 2 ↑(codeNumber n ⌈δ * ↑n⌉₊) / ↑n

theorem MetricCodes.Hamming.binaryRate_le_of_eventually {δ r : ℝ} {u : ℕ → ℝ} (hu : Filter.Tendsto u Filter.atTop (nhds r)) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, Real.logb 2 ↑(codeNumber n ⌈δ * ↑n⌉₊) / ↑n ≤ u n) : binaryRate δ ≤ r

theorem MetricCodes.Hamming.ceil_distance_le_dimension {δ : ℝ} (hδ : δ ≤ 1) (n : ℕ) : ⌈δ * ↑n⌉₊ ≤ n

theorem MetricCodes.Hamming.threshold_ceil_numerator_le_two {δ : ℝ} (hδ : δ ≤ 1) {n : ℕ} (hn : 0 < n) : 1 - threshold n ⌈δ * ↑n⌉₊ ≤ 2

noncomputable def MetricCodes.Hamming.spectralGap (δ a b : ℝ) : ℝ

The spectral gap used in the binary-code argument.

Equations

• MetricCodes.Hamming.spectralGap δ a b = (MetricCodes.hammingGamma a b - (1 - 2 * δ)) / 4

theorem MetricCodes.Hamming.spectralGap_pos {δ a b : ℝ} (h : Feasible δ a b) : 0 < spectralGap δ a b

theorem MetricCodes.Hamming.eventually_topEigenvalue_uniform_gap_ceil {δ a b : ℝ} (hδ : 0 ≤ δ) (h : Feasible δ a b) : ∀ᶠ (n : ℕ) in Filter.atTop, spectralGap δ a b < topEigenvalue n (transverseDegree b n) (longitudinalDegree a n) - threshold n ⌈δ * ↑n⌉₊

noncomputable def MetricCodes.Hamming.spectralPrefactor (δ a b : ℝ) : ℝ

The spectral prefactor used in the binary-code argument.

Equations

• MetricCodes.Hamming.spectralPrefactor δ a b = 2 / MetricCodes.Hamming.spectralGap δ a b

theorem MetricCodes.Hamming.spectralPrefactor_pos {δ a b : ℝ} (h : Feasible δ a b) : 0 < spectralPrefactor δ a b

theorem MetricCodes.Hamming.eventually_hamming_prefactor_le {δ a b : ℝ} (hδ : 0 ≤ δ) (hδ' : δ ≤ 1) (h : Feasible δ a b) : ∀ᶠ (n : ℕ) in Filter.atTop, (1 - threshold n ⌈δ * ↑n⌉₊) / (topEigenvalue n (transverseDegree b n) (longitudinalDegree a n) - threshold n ⌈δ * ↑n⌉₊) ≤ spectralPrefactor δ a b

theorem MetricCodes.Hamming.rateSet_nonempty_of_interior {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : (rateSet δ).Nonempty

theorem MetricCodes.Hamming.exists_positive_feasible_of_zero {δ a : ℝ} (h : Feasible δ a 0) : ∃ (b : ℝ), 0 < b ∧ Feasible δ a b

theorem MetricCodes.Hamming.binaryRate_le_of_eventually_windowFibreQuotient {δ a b C : ℝ} (hb : 0 < b) (hba : b < a) (ha : a ≤ 1 / 2) (hC : 0 < C) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(codeNumber n ⌈δ * ↑n⌉₊) ≤ C * windowFibreQuotient a b n) : binaryRate δ ≤ binaryEntropy a - binaryEntropy b

theorem MetricCodes.Hamming.binaryRate_le_of_positive_feasible_bound {δ a b : ℝ} (h : Feasible δ a b) (hb : 0 < b) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(codeNumber n ⌈δ * ↑n⌉₊) ≤ spectralPrefactor δ a b * windowFibreQuotient a b n) : binaryRate δ ≤ binaryEntropy a - binaryEntropy b

theorem MetricCodes.Hamming.binaryRate_le_variationalRate_of_positive_feasible_bounds {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) (hbound : ∀ ⦃a b : ℝ⦄, Feasible δ a b → 0 < b → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(codeNumber n ⌈δ * ↑n⌉₊) ≤ spectralPrefactor δ a b * windowFibreQuotient a b n) : binaryRate δ ≤ variationalRate δ

theorem MetricCodes.Hamming.finite_bound {n k L d : ℕ} (hn : 0 < n) (hd : 0 < d) (hkL : k < L) (hLn : L + k ≤ n) (hgap : threshold n d < topEigenvalue n k L) : ↑(codeNumber n d) ≤ (1 - threshold n d) / (topEigenvalue n k L - threshold n d) * (↑(ambientDimension n k L) / ↑(hammingFibreDimension n k))

theorem MetricCodes.Hamming.eventually_codeNumber_le_spectralPrefactor_mul_windowFibreQuotient {δ a b : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) (h : Feasible δ a b) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(codeNumber n ⌈δ * ↑n⌉₊) ≤ spectralPrefactor δ a b * windowFibreQuotient a b n

theorem MetricCodes.Hamming.binaryRate_le_variationalRate {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) : binaryRate δ ≤ variationalRate δ

noncomputable def MetricCodes.Johnson.binaryCodeFamily (n d : ℕ) : Finset (Finset (BinaryWord n))

The finite family of binary codes of length n and minimum distance at least d.

Equations

• MetricCodes.Johnson.binaryCodeFamily n d = {C ∈ Finset.univ.powerset | MetricCodes.IsBinaryCode d C}

@[simp]

theorem MetricCodes.Johnson.mem_binaryCodeFamily {n d : ℕ} (C : Finset (BinaryWord n)) : C ∈ binaryCodeFamily n d ↔ IsBinaryCode d C

theorem MetricCodes.Johnson.binaryCodeFamily_nonempty (n d : ℕ) : (binaryCodeFamily n d).Nonempty

noncomputable def MetricCodes.Johnson.binaryCodeNumber (n d : ℕ) : ℕ

The binary code number used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.binaryCodeNumber n d = (MetricCodes.Johnson.binaryCodeFamily n d).sup fun (C : Finset (MetricCodes.BinaryWord n)) => C.card

theorem MetricCodes.Johnson.card_le_binaryCodeNumber {n d : ℕ} (C : Finset (BinaryWord n)) (hC : IsBinaryCode d C) : C.card ≤ binaryCodeNumber n d

theorem MetricCodes.Johnson.exists_binaryCodeNumber (n d : ℕ) : ∃ (C : Finset (BinaryWord n)), IsBinaryCode d C ∧ C.card = binaryCodeNumber n d

noncomputable def MetricCodes.Johnson.shellCodeFamily (n w d : ℕ) : Finset (Finset (BinaryWord n))

The finite family of minimum-distance-d codes contained in the weight-w shell.

Equations

• MetricCodes.Johnson.shellCodeFamily n w d = {C ∈ (MetricCodes.weightShell n w).powerset | MetricCodes.IsBinaryCode d C}

@[simp]

theorem MetricCodes.Johnson.mem_shellCodeFamily {n w d : ℕ} (C : Finset (BinaryWord n)) : C ∈ shellCodeFamily n w d ↔ C ⊆ weightShell n w ∧ IsBinaryCode d C

theorem MetricCodes.Johnson.shellCodeFamily_nonempty (n w d : ℕ) : (shellCodeFamily n w d).Nonempty

noncomputable def MetricCodes.Johnson.shellCodeNumber (n w d : ℕ) : ℕ

The largest cardinality of a minimum-distance-d code in the weight-w shell.

Equations

• MetricCodes.Johnson.shellCodeNumber n w d = (MetricCodes.Johnson.shellCodeFamily n w d).sup fun (C : Finset (MetricCodes.BinaryWord n)) => C.card

theorem MetricCodes.Johnson.card_le_shellCodeNumber {n w d : ℕ} (C : Finset (BinaryWord n)) (hweight : C ⊆ weightShell n w) (hC : IsBinaryCode d C) : C.card ≤ shellCodeNumber n w d

theorem MetricCodes.Johnson.exists_shellCodeNumber (n w d : ℕ) : ∃ C ⊆ weightShell n w, IsBinaryCode d C ∧ C.card = shellCodeNumber n w d

theorem MetricCodes.Johnson.bassalygo_elias (n w d : ℕ) : binaryCodeNumber n d * n.choose w ≤ 2 ^ n * shellCodeNumber n w d

theorem MetricCodes.Johnson.bassalygo_elias_real {n w d : ℕ} (hw : w ≤ n) : ↑(binaryCodeNumber n d) ≤ 2 ^ n / ↑(n.choose w) * ↑(shellCodeNumber n w d)

theorem MetricCodes.Johnson.binaryCodeNumber_eq_hamming (n d : ℕ) : binaryCodeNumber n d = Hamming.codeNumber n d

def MetricCodes.Johnson.words {n w : ℕ} (C : Finset (JohnsonSphere n w)) : Finset (BinaryWord n)

Forget the weight proof on each point of a finite Johnson-sphere code.

Equations

• MetricCodes.Johnson.words C = Finset.image Subtype.val C

def MetricCodes.Johnson.IsCode {n w : ℕ} (d : ℕ) (C : Finset (JohnsonSphere n w)) : Prop

The minimum-distance condition on the underlying binary words of a Johnson-sphere code.

Equations

• MetricCodes.Johnson.IsCode d C = MetricCodes.IsBinaryCode d (MetricCodes.Johnson.words C)

def MetricCodes.Johnson.asSubtype {n w : ℕ} (C : Finset (BinaryWord n)) (hweight : C ⊆ weightShell n w) : Finset (JohnsonSphere n w)

Regard a code contained in the weight-w shell as a finite set of Johnson-sphere points.

Equations

• MetricCodes.Johnson.asSubtype C hweight = Finset.image (fun (x : ↥C) => ⟨↑x, ⋯⟩) C.attach

theorem MetricCodes.Johnson.card_asSubtype {n w : ℕ} (C : Finset (BinaryWord n)) (hweight : C ⊆ weightShell n w) : (asSubtype C hweight).card = C.card

theorem MetricCodes.Johnson.words_asSubtype {n w : ℕ} (C : Finset (BinaryWord n)) (hweight : C ⊆ weightShell n w) : words (asSubtype C hweight) = C

theorem MetricCodes.Johnson.isCode_asSubtype {n w d : ℕ} (C : Finset (BinaryWord n)) (hweight : C ⊆ weightShell n w) (hC : IsBinaryCode d C) : IsCode d (asSubtype C hweight)

noncomputable def MetricCodes.Johnson.correlation {n w : ℕ} (x y : JohnsonSphere n w) : ℝ

The correlation used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.correlation x y = 1 - ↑n * ↑(MetricCodes.johnsonDist x y) / (↑w * ↑(n - w))

@[simp]

theorem MetricCodes.Johnson.correlation_self {n w : ℕ} (x : JohnsonSphere n w) : correlation x x = 1

noncomputable def MetricCodes.Johnson.threshold (n w d : ℕ) : ℝ

The threshold used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.threshold n w d = 1 - ↑n * ↑d / (2 * ↑w * ↑(n - w))

theorem MetricCodes.Johnson.correlation_eq_hamming {n w : ℕ} (hw : 0 < w) (hwn : w < n) (x y : JohnsonSphere n w) : correlation x y = 1 - ↑n * ↑(hammingDist ↑x ↑y) / (2 * ↑w * ↑(n - w))

theorem MetricCodes.Johnson.threshold_lt_one {n w d : ℕ} (hw : 0 < w) (hwn : w < n) (hd : 0 < d) : threshold n w d < 1

theorem MetricCodes.Johnson.correlation_le_threshold {n w d : ℕ} (hw : 0 < w) (hwn : w < n) {x y : JohnsonSphere n w} (hd : d ≤ hammingDist ↑x ↑y) : correlation x y ≤ threshold n w d

theorem MetricCodes.Johnson.correlation_le_threshold_of_code {n w d : ℕ} (hw : 0 < w) (hwn : w < n) {C : Finset (JohnsonSphere n w)} (hC : IsCode d C) {x y : JohnsonSphere n w} (hx : x ∈ C) (hy : y ∈ C) (hxy : x ≠ y) : correlation x y ≤ threshold n w d

def MetricCodes.Johnson.coordinateIndicator {n : ℕ} (x : BinaryWord n) (i : Fin n) : ℝ

The coordinate indicator used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.coordinateIndicator x i = if i ∈ MetricCodes.wordSupport x then 1 else 0

theorem MetricCodes.Johnson.sum_coordinateIndicator {n : ℕ} (x : BinaryWord n) : ∑ i : Fin n, coordinateIndicator x i = ↑(binaryWeight x)

theorem MetricCodes.Johnson.sum_coordinateIndicator_mul {n : ℕ} (x y : BinaryWord n) : ∑ i : Fin n, coordinateIndicator x i * coordinateIndicator y i = ↑(wordSupport x ∩ wordSupport y).card

theorem MetricCodes.Johnson.centered_coordinate_inner_sum {n w : ℕ} (hn : 0 < n) (x y : JohnsonSphere n w) : ∑ i : Fin n, (coordinateIndicator (↑x) i - ↑w / ↑n) * (coordinateIndicator (↑y) i - ↑w / ↑n) = ↑(wordSupport ↑x ∩ wordSupport ↑y).card - ↑w ^ 2 / ↑n

noncomputable def MetricCodes.Johnson.geometricAxis {n w : ℕ} (x : JohnsonSphere n w) : Ambient n

The geometric axis used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.geometricAxis x = WithLp.toLp 2 fun (i : Fin n) => √(↑n / (↑w * ↑(n - w))) * (MetricCodes.Johnson.coordinateIndicator (↑x) i - ↑w / ↑n)

theorem MetricCodes.Johnson.geometricAxis_inner {n w : ℕ} (hw : 0 < w) (hwn : w < n) (x y : JohnsonSphere n w) : inner ℝ (geometricAxis x) (geometricAxis y) = correlation x y

@[reducible, inline]

abbrev MetricCodes.Johnson.SupportCoordinates {n w : ℕ} (x : JohnsonSphere n w) : Type

The support coordinates used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.SupportCoordinates x = ↥(MetricCodes.wordSupport ↑x)

@[reducible, inline]

abbrev MetricCodes.Johnson.ComplementCoordinates {n w : ℕ} (x : JohnsonSphere n w) : Type

The complement coordinates used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.ComplementCoordinates x = ↥(Finset.univ \ MetricCodes.wordSupport ↑x)

noncomputable def MetricCodes.Johnson.supportCoordinateEquiv {n w : ℕ} (x : JohnsonSphere n w) : SupportCoordinates x ≃ Fin w

The support coordinate equiv used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.supportCoordinateEquiv x = Fintype.equivOfCardEq ⋯

noncomputable def MetricCodes.Johnson.complementCoordinateEquiv {n w : ℕ} (x : JohnsonSphere n w) : ComplementCoordinates x ≃ Fin (n - w)

The complement coordinate equiv used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.complementCoordinateEquiv x = Fintype.equivOfCardEq ⋯

@[reducible, inline]

abbrev MetricCodes.Johnson.HarmonicFibreIndex (n w p q : ℕ) : Type

The harmonic fibre index used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.HarmonicFibreIndex n w p q = (Fin (MetricCodes.hammingFibreDimension w p) × Fin (MetricCodes.hammingFibreDimension (n - w) q))

noncomputable def MetricCodes.Johnson.harmonicFibreIndexEquiv (n w p q : ℕ) : HarmonicFibreIndex n w p q ≃ Fin (johnsonFibreDimension n w p q)

The harmonic fibre index equiv used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.harmonicFibreIndexEquiv n w p q = Fintype.equivOfCardEq ⋯

@[reducible, inline]

abbrev MetricCodes.Johnson.ShellWindowIndex (n p q L : ℕ) : Type

The shell window index used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.ShellWindowIndex n p q L = ((i : Fin (L - (p + q) + 1)) × Fin (MetricCodes.booleanHarmonicDimension n (p + q + ↑i)))

theorem MetricCodes.Johnson.shellWindowIndex_card (n p q L : ℕ) (hfirst : p + q ≤ L) : Fintype.card (ShellWindowIndex n p q L) = johnsonAmbientDimension n (p + q) L

noncomputable def MetricCodes.Johnson.shellWindowIndexEquiv (n p q L : ℕ) (hfirst : p + q ≤ L) : ShellWindowIndex n p q L ≃ Fin (johnsonAmbientDimension n (p + q) L)

The shell window index equiv used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.shellWindowIndexEquiv n p q L hfirst = Fintype.equivOfCardEq ⋯

@[reducible, inline]

abbrev MetricCodes.Johnson.Index (p q L : ℕ) : Type

The index used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Index p q L = Fin (L - (p + q) + 1)

@[reducible, inline]

abbrev MetricCodes.Johnson.Space (p q L : ℕ) : Type

The space used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Space p q L = EuclideanSpace ℝ (MetricCodes.Johnson.Index p q L)

noncomputable def MetricCodes.Johnson.matrix (n w p q L : ℕ) : Matrix (Index p q L) (Index p q L) ℝ

The matrix used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.matrix n w p q L = MetricCodes.johnsonJacobiMatrix n w p q L

theorem MetricCodes.Johnson.matrix_hermitian (n w p q L : ℕ) : (matrix n w p q L).IsHermitian

noncomputable def MetricCodes.Johnson.operator (n w p q L : ℕ) : Space p q L →ₗ[ℝ] Space p q L

The operator used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.operator n w p q L = Matrix.toEuclideanLin (MetricCodes.Johnson.matrix n w p q L)

theorem MetricCodes.Johnson.operator_isSymmetric (n w p q L : ℕ) : (operator n w p q L).IsSymmetric

noncomputable def MetricCodes.Johnson.continuousOperator (n w p q L : ℕ) : Space p q L →L[ℝ] Space p q L

The continuous operator used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.continuousOperator n w p q L = LinearMap.toContinuousLinearMap (MetricCodes.Johnson.operator n w p q L)

noncomputable def MetricCodes.Johnson.rayleigh (n w p q L : ℕ) (x : Space p q L) : ℝ

The rayleigh used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.rayleigh n w p q L x = (MetricCodes.Johnson.continuousOperator n w p q L).rayleighQuotient x

theorem MetricCodes.Johnson.rayleigh_bddAbove (n w p q L : ℕ) : BddAbove (Set.range fun (x : { x : Space p q L // x ≠ 0 }) => rayleigh n w p q L ↑x)

noncomputable def MetricCodes.Johnson.topEigenvalue (n w p q L : ℕ) : ℝ

The top eigenvalue used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.topEigenvalue n w p q L = ⨆ (x : { x : MetricCodes.Johnson.Space p q L // x ≠ 0 }), MetricCodes.Johnson.rayleigh n w p q L ↑x

theorem MetricCodes.Johnson.rayleigh_le_top (n w p q L : ℕ) (x : Space p q L) (hx : x ≠ 0) : rayleigh n w p q L x ≤ topEigenvalue n w p q L

theorem MetricCodes.Johnson.topEigenvalue_hasEigenvalue (n w p q L : ℕ) : Module.End.HasEigenvalue (operator n w p q L) (topEigenvalue n w p q L)

theorem MetricCodes.Johnson.exists_topEigenvector (n w p q L : ℕ) : ∃ (x : Space p q L), x ≠ 0 ∧ (operator n w p q L) x = topEigenvalue n w p q L • x

theorem MetricCodes.Johnson.rayleigh_eq_inner (n w p q L : ℕ) (x : Space p q L) : rayleigh n w p q L x = inner ℝ ((operator n w p q L) x) x / ‖x‖ ^ 2

structure MetricCodes.Johnson.AdmissibleDegrees (n w p q L : ℕ) : Prop

Data encoding the admissible degrees construction.

• weight_pos : 0 < w
• weight_lt : w < n
• weight_half : 2 * w ≤ n
• support_half : 2 * p ≤ w
• complement_half : 2 * q ≤ n - w
• first_le : p + q ≤ L
• last_le : L ≤ johnsonLastDegree n w p q

theorem MetricCodes.Johnson.AdmissibleDegrees.terminal_le_weight {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : L ≤ w

theorem MetricCodes.Johnson.AdmissibleDegrees.terminal_le_half {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : L ≤ n / 2

theorem MetricCodes.Johnson.booleanHarmonicDimension_pos {n k : ℕ} (hk : 2 * k ≤ n) : 0 < booleanHarmonicDimension n k

theorem MetricCodes.Johnson.AdmissibleDegrees.fibreDimension_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : 0 < johnsonFibreDimension n w p q

theorem MetricCodes.Johnson.ambientDimension_eq {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : johnsonAmbientDimension n (p + q) L = n.choose L - precedingBinomial n (p + q)

theorem MetricCodes.Johnson.zonalDiagonal_eq {n w j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hj : j ≤ w) : johnsonZonalDiagonal n w j = johnsonM n w ^ 2 * ↑j * (↑n - ↑j + 1) / (↑w * ↑(n - w) * johnsonJ n j * (johnsonJ n j + 1))

theorem MetricCodes.Johnson.zonalDiagonal_pos {n w j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hj : 0 < j) (hjw : j ≤ w) : 0 < johnsonZonalDiagonal n w j

theorem MetricCodes.Johnson.associatedEdge_pos {n w p q j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hfirst : p + q ≤ j) (hlast : j < johnsonLastDegree n w p q) : 0 < johnsonEdge n w p q j

theorem MetricCodes.Johnson.zonalEdge_pos {n w j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hj : j < w) : 0 < johnsonZonalEdge n w j

theorem MetricCodes.Johnson.hattedDiagonal_nonneg {n w p q j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hj : j ≤ w) : 0 ≤ johnsonHattedDiagonal n w p q j

theorem MetricCodes.Johnson.hattedEdge_pos {n w p q j : ℕ} (hw : 0 < w) (hhalf : 2 * w < n) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hfirst : p + q ≤ j) (hlast : j < johnsonLastDegree n w p q) : 0 < johnsonHattedEdge n w p q j

theorem MetricCodes.Johnson.matrix_entry_nonneg {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (i j : Index p q L) : 0 ≤ matrix n w p q L i j

@[reducible, inline]

abbrev MetricCodes.Johnson.coordinateAbs (p q L : ℕ) (x : Space p q L) : Space p q L

The coordinate abs used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.coordinateAbs p q L x = MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs x

theorem MetricCodes.Johnson.coordinateAbs_norm (p q L : ℕ) (x : Space p q L) : ‖coordinateAbs p q L x‖ = ‖x‖

theorem MetricCodes.Johnson.coordinateAbs_ne_zero (p q L : ℕ) {x : Space p q L} (hx : x ≠ 0) : coordinateAbs p q L x ≠ 0

theorem MetricCodes.Johnson.inner_le_inner_coordinateAbs {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : Space p q L) : inner ℝ ((operator n w p q L) x) x ≤ inner ℝ ((operator n w p q L) (coordinateAbs p q L x)) (coordinateAbs p q L x)

theorem MetricCodes.Johnson.rayleigh_le_coordinateAbs {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : Space p q L) : rayleigh n w p q L x ≤ rayleigh n w p q L (coordinateAbs p q L x)

theorem MetricCodes.Johnson.rayleigh_eq_of_eigenvector (n w p q L : ℕ) (x : Space p q L) (hx : x ≠ 0) (eigenvalue : ℝ) (heigen : (operator n w p q L) x = eigenvalue • x) : rayleigh n w p q L x = eigenvalue

theorem MetricCodes.Johnson.coordinateAbs_top_rayleigh {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : Space p q L) (hx : x ≠ 0) (heigen : (operator n w p q L) x = topEigenvalue n w p q L • x) : rayleigh n w p q L (coordinateAbs p q L x) = topEigenvalue n w p q L

theorem MetricCodes.Johnson.exists_nonnegative_topEigenvector {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) : ∃ (x : Space p q L), x ≠ 0 ∧ (operator n w p q L) x = topEigenvalue n w p q L • x ∧ ∀ (i : Index p q L), 0 ≤ x.ofLp i

theorem MetricCodes.Johnson.exists_nonnegative_unit_topEigenvector {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) : ∃ (x : Space p q L), ‖x‖ = 1 ∧ (operator n w p q L) x = topEigenvalue n w p q L • x ∧ ∀ (i : Index p q L), 0 ≤ x.ofLp i

theorem MetricCodes.Johnson.matrix_adjacent_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (i j : Index p q L) (hadjacent : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : 0 < matrix n w p q L i j

theorem MetricCodes.Johnson.nonnegative_eigenvector_zero_propagates {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (eigenvalue : ℝ) (heigen : (operator n w p q L) v = eigenvalue • v) (hnonnegative : ∀ (i : Index p q L), 0 ≤ v.ofLp i) (i j : Index p q L) (hzero : v.ofLp i = 0) (hadjacent : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : v.ofLp j = 0

theorem MetricCodes.Johnson.nonnegative_eigenvector_coordinate_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (eigenvalue : ℝ) (heigen : (operator n w p q L) v = eigenvalue • v) (hnonnegative : ∀ (i : Index p q L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) (i : Index p q L) : 0 < v.ofLp i

theorem MetricCodes.Johnson.exists_positive_unit_topEigenvector {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) : ∃ (v : Space p q L), ‖v‖ = 1 ∧ (operator n w p q L) v = topEigenvalue n w p q L • v ∧ ∀ (i : Index p q L), 0 < v.ofLp i

theorem MetricCodes.Johnson.topEigenvalue_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (hwindow : p + q < L) : 0 < topEigenvalue n w p q L

theorem MetricCodes.Johnson.johnsonWindowHarmonicDimension_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (i : Index p q L) : 0 < booleanHarmonicDimension n (p + q + ↑i)

noncomputable def MetricCodes.Johnson.johnsonRecurrenceWeight (n : ℕ) : ℕ → (p q L : ℕ) → (v : Space p q L) → (i : Index p q L) → ℝ

The johnson recurrence weight used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.johnsonRecurrenceWeight n x✝ p q L v i = √↑(MetricCodes.booleanHarmonicDimension n (p + q + ↑i)) * v.ofLp i

noncomputable def MetricCodes.Johnson.johnsonSourceChannelCoefficient (n w p q L : ℕ) (m i : Index p q L) : ℝ

The johnson source channel coefficient used in the Johnson-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_mul_sqrt_dimension {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (m i : Index p q L) : johnsonSourceChannelCoefficient n w p q L m i * √↑(booleanHarmonicDimension n (p + q + ↑i)) = matrix n w p q L m i * √↑(booleanHarmonicDimension n (p + q + ↑m))

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_nonneg {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (m i : Index p q L) : 0 ≤ johnsonSourceChannelCoefficient n w p q L m i

theorem MetricCodes.Johnson.johnsonRecurrenceWeight_pos_of_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (i : Index p q L) : 0 < johnsonRecurrenceWeight n w p q L v i

theorem MetricCodes.Johnson.johnsonRecurrenceWeight_eigenrecurrence {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (lam : ℝ) (heigen : (operator n w p q L) v = lam • v) (m : Index p q L) : ∑ i : Index p q L, johnsonSourceChannelCoefficient n w p q L m i * johnsonRecurrenceWeight n w p q L v i = lam * johnsonRecurrenceWeight n w p q L v m

noncomputable def MetricCodes.Johnson.johnsonAdjacentBlockCoefficient (n w p q L : ℕ) (v : Space p q L) (lam : ℝ) (target source : Index p q L) : ℝ

The johnson adjacent block coefficient used in the Johnson-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Johnson.johnsonAdjacentBlockCoefficient_sq {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (target source : Index p q L) : johnsonAdjacentBlockCoefficient n w p q L v lam target source ^ 2 = johnsonSourceChannelCoefficient n w p q L source target * johnsonRecurrenceWeight n w p q L v target / (lam * johnsonRecurrenceWeight n w p q L v source)

theorem MetricCodes.Johnson.johnsonAdjacentBlockCoefficient_sq_sum {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (operator n w p q L) v = lam • v) (source : Index p q L) : ∑ target : Index p q L, johnsonAdjacentBlockCoefficient n w p q L v lam target source ^ 2 = 1

noncomputable def MetricCodes.Johnson.johnsonRecurrenceNormalization (n w p q L : ℕ) (v : Space p q L) : ℝ

The sum of the Johnson recurrence weights over the admissible index range.

Equations

• MetricCodes.Johnson.johnsonRecurrenceNormalization n w p q L v = ∑ i : MetricCodes.Johnson.Index p q L, MetricCodes.Johnson.johnsonRecurrenceWeight n w p q L v i

noncomputable def MetricCodes.Johnson.johnsonFibreAmplitude (n w p q L : ℕ) (v : Space p q L) (i : Index p q L) : ℝ

The johnson fibre amplitude used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.johnsonFibreAmplitude n w p q L v i = √(MetricCodes.Johnson.johnsonRecurrenceWeight n w p q L v i / MetricCodes.Johnson.johnsonRecurrenceNormalization n w p q L v)

theorem MetricCodes.Johnson.johnsonRecurrenceNormalization_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) : 0 < johnsonRecurrenceNormalization n w p q L v

theorem MetricCodes.Johnson.johnsonFibreAmplitude_sq {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (i : Index p q L) : johnsonFibreAmplitude n w p q L v i ^ 2 = johnsonRecurrenceWeight n w p q L v i / johnsonRecurrenceNormalization n w p q L v

theorem MetricCodes.Johnson.johnsonFibreAmplitude_sq_sum {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) : ∑ i : Index p q L, johnsonFibreAmplitude n w p q L v i ^ 2 = 1

theorem MetricCodes.Johnson.johnsonFibreAmplitude_pos_of_pos {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (i : Index p q L) : 0 < johnsonFibreAmplitude n w p q L v i

theorem MetricCodes.Johnson.johnsonAdjacentBlockCoefficient_amplitude_identity {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (target source : Index p q L) : johnsonAdjacentBlockCoefficient n w p q L v lam target source * johnsonFibreAmplitude n w p q L v target * √(johnsonSourceChannelCoefficient n w p q L source target) = johnsonAdjacentBlockCoefficient n w p q L v lam target source ^ 2 * √lam * johnsonFibreAmplitude n w p q L v source

theorem MetricCodes.Johnson.johnsonAdjacentBlockCoefficient_amplitude_sum {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (hv : ∀ (i : Index p q L), 0 < v.ofLp i) (lam : ℝ) (hlam : 0 < lam) (heigen : (operator n w p q L) v = lam • v) (source : Index p q L) : ∑ target : Index p q L, johnsonAdjacentBlockCoefficient n w p q L v lam target source * johnsonFibreAmplitude n w p q L v target * √(johnsonSourceChannelCoefficient n w p q L source target) = √lam * johnsonFibreAmplitude n w p q L v source

structure MetricCodes.Johnson.ProjectionGram (n w p q L : ℕ) : Type

Data encoding the projection gram construction.

• projections : ProjectionFamily (JohnsonSphere n w) (johnsonAmbientDimension n (p + q) L) (johnsonFibreDimension n w p q)

  The projections component.

• feature : JohnsonSphere n w → EuclideanSpace ℝ (Fin (n * johnsonAmbientDimension n (p + q) L * johnsonAmbientDimension n (p + q) L))

  The feature component.

• gram (x y : JohnsonSphere n w) : inner ℝ (self.feature x) (self.feature y) = (correlation x y - topEigenvalue n w p q L) * self.projections.overlap x y

theorem MetricCodes.Johnson.finite_bound_of_projection_gram {n w p q L d : ℕ} (hdegree : AdmissibleDegrees n w p q L) (hd : 0 < d) (data : ProjectionGram n w p q L) (C : Finset (JohnsonSphere n w)) (hC : IsCode d C) (hgap : threshold n w d < topEigenvalue n w p q L) : ↑C.card ≤ (1 - threshold n w d) / (topEigenvalue n w p q L - threshold n w d) * (↑(johnsonAmbientDimension n (p + q) L) / ↑(johnsonFibreDimension n w p q))

theorem MetricCodes.Johnson.finite_shellCodeNumber_bound_of_projection_gram {n w p q L d : ℕ} (hdegree : AdmissibleDegrees n w p q L) (hd : 0 < d) (data : ProjectionGram n w p q L) (hgap : threshold n w d < topEigenvalue n w p q L) : ↑(shellCodeNumber n w d) ≤ (1 - threshold n w d) / (topEigenvalue n w p q L - threshold n w d) * (↑(johnsonAmbientDimension n (p + q) L) / ↑(johnsonFibreDimension n w p q))

theorem MetricCodes.Johnson.finite_binaryCodeNumber_bound_of_projection_gram {n w p q L d : ℕ} (hdegree : AdmissibleDegrees n w p q L) (hd : 0 < d) (data : ProjectionGram n w p q L) (hgap : threshold n w d < topEigenvalue n w p q L) : ↑(binaryCodeNumber n d) ≤ 2 ^ n / ↑(n.choose w) * ((1 - threshold n w d) / (topEigenvalue n w p q L - threshold n w d) * (↑(johnsonAmbientDimension n (p + q) L) / ↑(johnsonFibreDimension n w p q)))

def MetricCodes.Johnson.centeredEta (α β γ : ℝ) : ℝ

The centered eta used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.centeredEta α β γ = 1 - 2 * α + 2 * β - 2 * γ

noncomputable def MetricCodes.Johnson.spectralLimit (α β γ u : ℝ) : ℝ

The spectral limit used in the Johnson-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Johnson.sqrt_one_sub_centeredDegree_sq {u : ℝ} (hu : 0 < u) (hhalf : u < 1 / 2) : √(1 - (1 - 2 * u) ^ 2) = 2 * √(u * (1 - u))

theorem MetricCodes.Johnson.zero_fibre_spectral_algebra (z m s : ℝ) (hz : z ≠ 0) (hm : 1 - m ^ 2 ≠ 0) (hs : s ≠ 0) (hplus : 1 + 2 * s ≠ 0) (hsquare : 4 * s ^ 2 = 1 - z ^ 2) : 1 - ((m - m * z ^ 2) ^ 2 / (z ^ 2 * (1 - m ^ 2) * (1 - z ^ 2)) + (z ^ 2 - m ^ 2) * (1 - z ^ 2) / (z ^ 2 * (1 - m ^ 2) * (2 * s))) = (z ^ 2 - m ^ 2) / ((1 - m ^ 2) * (1 + 2 * s))

theorem MetricCodes.Johnson.spectralLimit_zero_fibre_boundary {α u : ℝ} (hu : 0 < u) (hua : u < α) (ha : α < 1 / 2) : 1 - spectralLimit α 0 0 u = (α * (1 - α) - u * (1 - u)) / (α * (1 - α) * (1 + 2 * √(u * (1 - u))))

noncomputable def MetricCodes.Johnson.asymptoticThreshold (δ α : ℝ) : ℝ

The asymptotic threshold used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.asymptoticThreshold δ α = 1 - δ / (2 * α * (1 - α))

noncomputable def MetricCodes.Johnson.rankPenalty (α β γ : ℝ) : ℝ

The rank penalty used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.rankPenalty α β γ = α * MetricCodes.binaryEntropy (β / α) + (1 - α) * MetricCodes.binaryEntropy (γ / (1 - α))

noncomputable def MetricCodes.Johnson.shellRate (α β γ u : ℝ) : ℝ

The shell rate used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.shellRate α β γ u = 1 - MetricCodes.binaryEntropy α + MetricCodes.binaryEntropy u - MetricCodes.Johnson.rankPenalty α β γ

theorem MetricCodes.Johnson.binaryEntropy_eq_binEntropy_div_log (u : ℝ) : binaryEntropy u = Real.binEntropy u / Real.log 2

theorem MetricCodes.Johnson.binaryEntropy_le_one (u : ℝ) : binaryEntropy u ≤ 1

structure MetricCodes.Johnson.AsymptoticParameters (δ α β γ u : ℝ) : Prop

Data encoding the asymptotic parameters construction.

• distance_pos : 0 < δ
• distance_lt_half : δ < 1 / 2
• weight_gt_distance : δ / 2 < α
• weight_lt_half : α < 1 / 2
• support_nonneg : 0 ≤ β
• support_lt_half : β < α / 2
• complement_nonneg : 0 ≤ γ
• complement_lt_half : γ < (1 - α) / 2
• first_lt_degree : β + γ < u
• degree_lt_weight : u < α
• degree_lt_left : u < α - β + γ
• degree_lt_right : u < 1 - α + β - γ

theorem MetricCodes.Johnson.AsymptoticParameters.weight_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < α

theorem MetricCodes.Johnson.AsymptoticParameters.weight_complement_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - α

theorem MetricCodes.Johnson.AsymptoticParameters.degree_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < u

theorem MetricCodes.Johnson.AsymptoticParameters.centeredDegree_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - 2 * u

theorem MetricCodes.Johnson.AsymptoticParameters.centeredWeight_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - 2 * α

theorem MetricCodes.Johnson.AsymptoticParameters.centeredSigma_gt_degree {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 1 - 2 * u < 1 - 2 * β - 2 * γ

theorem MetricCodes.Johnson.AsymptoticParameters.centeredSigma_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - 2 * β - 2 * γ

theorem MetricCodes.Johnson.AsymptoticParameters.centeredEta_lt_degree {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : centeredEta α β γ < 1 - 2 * u

theorem MetricCodes.Johnson.AsymptoticParameters.neg_degree_lt_centeredEta {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : -(1 - 2 * u) < centeredEta α β γ

theorem MetricCodes.Johnson.AsymptoticParameters.one_sub_centeredWeight_sq_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - (1 - 2 * α) ^ 2

theorem MetricCodes.Johnson.AsymptoticParameters.one_sub_centeredDegree_sq_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < 1 - (1 - 2 * u) ^ 2

theorem MetricCodes.Johnson.AsymptoticParameters.degree_sq_sub_eta_sq_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < (1 - 2 * u) ^ 2 - centeredEta α β γ ^ 2

theorem MetricCodes.Johnson.AsymptoticParameters.sigma_sq_sub_degree_sq_pos {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : 0 < (1 - 2 * β - 2 * γ) ^ 2 - (1 - 2 * u) ^ 2

theorem MetricCodes.Johnson.AsymptoticParameters.rankPenalty_le_one {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : rankPenalty α β γ ≤ 1

theorem MetricCodes.Johnson.AsymptoticParameters.shellRate_lower {δ α β γ u : ℝ} (h : AsymptoticParameters δ α β γ u) : -1 ≤ shellRate α β γ u

@[simp]

theorem MetricCodes.Johnson.shellRate_zero_fibre (α u : ℝ) : shellRate α 0 0 u = 1 - binaryEntropy α + binaryEntropy u

def MetricCodes.Johnson.IsSpectrallyFeasible (δ α β γ u : ℝ) : Prop

The predicate asserting spectrally feasible.

Equations

• MetricCodes.Johnson.IsSpectrallyFeasible δ α β γ u = (MetricCodes.Johnson.asymptoticThreshold δ α < MetricCodes.Johnson.spectralLimit α β γ u)

def MetricCodes.Johnson.Feasible (δ α β γ u : ℝ) : Prop

The feasible used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Feasible δ α β γ u = (MetricCodes.Johnson.AsymptoticParameters δ α β γ u ∧ MetricCodes.Johnson.IsSpectrallyFeasible δ α β γ u)

def MetricCodes.Johnson.rateSet (δ : ℝ) : Set ℝ

The rate set used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.rateSet δ = {r : ℝ | ∃ (α : ℝ) (β : ℝ) (γ : ℝ) (u : ℝ), MetricCodes.Johnson.Feasible δ α β γ u ∧ r = MetricCodes.Johnson.shellRate α β γ u}

theorem MetricCodes.Johnson.rateSet_bddBelow (δ : ℝ) : BddBelow (rateSet δ)

noncomputable def MetricCodes.Johnson.variationalRate (δ : ℝ) : ℝ

The variational rate used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.variationalRate δ = sInf (MetricCodes.Johnson.rateSet δ)

theorem MetricCodes.Johnson.variationalRate_le_of_feasible {δ α β γ u : ℝ} (h : Feasible δ α β γ u) : variationalRate δ ≤ shellRate α β γ u

noncomputable def MetricCodes.Johnson.mrrwG (v : ℝ) : ℝ

The mrrw g used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.mrrwG v = MetricCodes.binaryEntropy ((1 - √(1 - v)) / 2)

@[simp]

theorem MetricCodes.Johnson.mrrwG_one : mrrwG 1 = 1

theorem MetricCodes.Johnson.mrrwG_continuous : Continuous mrrwG

theorem MetricCodes.Johnson.mrrwG_nonneg {v : ℝ} (hv : 0 ≤ v) : 0 ≤ mrrwG v

noncomputable def MetricCodes.Johnson.mrrwObjective (δ r : ℝ) : ℝ

The mrrw objective used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.mrrwObjective δ r = 1 + MetricCodes.Johnson.mrrwG (r ^ 2) - MetricCodes.Johnson.mrrwG (r ^ 2 + 2 * δ * r + 2 * δ)

theorem MetricCodes.Johnson.mrrwObjective_continuous (δ : ℝ) : Continuous (mrrwObjective δ)

theorem MetricCodes.Johnson.mrrwObjective_endpoint {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : mrrwObjective δ (1 - 2 * δ) = Hamming.classicalRate δ

theorem MetricCodes.Johnson.mrrwG_variance {u : ℝ} (hu : u ≤ 1 / 2) : mrrwG (4 * u * (1 - u)) = binaryEntropy u

theorem MetricCodes.Johnson.zero_fibre_boundary_variance {δ α u : ℝ} (hu : 0 < u) (hua : u < α) (ha : α < 1 / 2) (hboundary : spectralLimit α 0 0 u = asymptoticThreshold δ α) : 4 * α * (1 - α) = (2 * √(u * (1 - u))) ^ 2 + 2 * δ * (2 * √(u * (1 - u))) + 2 * δ

theorem MetricCodes.Johnson.mrrwObjective_zero_fibre_boundary {δ α u : ℝ} (hu : 0 < u) (hua : u < α) (ha : α < 1 / 2) (hboundary : spectralLimit α 0 0 u = asymptoticThreshold δ α) : mrrwObjective δ (2 * √(u * (1 - u))) = shellRate α 0 0 u

def MetricCodes.Johnson.mrrwRateSet (δ : ℝ) : Set ℝ

The values of the MRRW objective as r ranges from zero to 1 - 2 * δ.

Equations

• MetricCodes.Johnson.mrrwRateSet δ = {t : ℝ | ∃ (r : ℝ), 0 ≤ r ∧ r ≤ 1 - 2 * δ ∧ t = MetricCodes.Johnson.mrrwObjective δ r}

theorem MetricCodes.Johnson.mrrwRateSet_bddBelow (δ : ℝ) : BddBelow (mrrwRateSet δ)

noncomputable def MetricCodes.Johnson.mrrwRate (δ : ℝ) : ℝ

The mrrw rate used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.mrrwRate δ = sInf (MetricCodes.Johnson.mrrwRateSet δ)

theorem MetricCodes.Johnson.mrrwRate_le_objective {δ r : ℝ} (hr : 0 ≤ r) (hupper : r ≤ 1 - 2 * δ) : mrrwRate δ ≤ mrrwObjective δ r

theorem MetricCodes.Johnson.exists_mrrw_minimizer {δ : ℝ} (hhalf : δ ≤ 1 / 2) : ∃ (r : ℝ), 0 ≤ r ∧ r ≤ 1 - 2 * δ ∧ ∀ (s : ℝ), 0 ≤ s → s ≤ 1 - 2 * δ → mrrwObjective δ r ≤ mrrwObjective δ s

theorem MetricCodes.Johnson.mrrwRate_eq_objective_of_minimizer {δ r : ℝ} (hr : 0 ≤ r) (hupper : r ≤ 1 - 2 * δ) (hmin : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 - 2 * δ → mrrwObjective δ r ≤ mrrwObjective δ s) : mrrwRate δ = mrrwObjective δ r

theorem MetricCodes.Johnson.mrrwRate_le_classicalRate {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : mrrwRate δ ≤ Hamming.classicalRate δ

theorem MetricCodes.Johnson.mrrw_endpoint_dichotomy {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : mrrwRate δ < Hamming.classicalRate δ ∨ mrrwRate δ = Hamming.classicalRate δ

noncomputable def MetricCodes.Johnson.combinedVariationalRate (δ : ℝ) : ℝ

The combined variational rate used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.combinedVariationalRate δ = min (MetricCodes.Hamming.variationalRate δ) (MetricCodes.Johnson.variationalRate δ)

theorem MetricCodes.Johnson.combinedVariationalRate_le_hamming (δ : ℝ) : combinedVariationalRate δ ≤ Hamming.variationalRate δ

theorem MetricCodes.Johnson.combinedVariationalRate_le_shell (δ : ℝ) : combinedVariationalRate δ ≤ variationalRate δ

theorem MetricCodes.Johnson.combinedVariationalRate_lt_mrrw_of_endpoint {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) (hendpoint : mrrwRate δ = Hamming.classicalRate δ) : combinedVariationalRate δ < mrrwRate δ