Binary-code asymptotics

Asymptotic Johnson-scheme estimates and the binary-code variational bound.

noncomputable def MetricCodes.Johnson.Asymptotics.shellWeight (a : ℝ) (n : ℕ) : ℕ

The shell weight used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.shellWeight a n = MetricCodes.Hamming.longitudinalDegree a n

noncomputable def MetricCodes.Johnson.Asymptotics.supportDegree (b : ℝ) (n : ℕ) : ℕ

The support degree used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.supportDegree b n = MetricCodes.Hamming.longitudinalDegree b n

noncomputable def MetricCodes.Johnson.Asymptotics.complementDegree (g : ℝ) (n : ℕ) : ℕ

The complement degree used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.complementDegree g n = MetricCodes.Hamming.longitudinalDegree g n

noncomputable def MetricCodes.Johnson.Asymptotics.terminalDegree (u : ℝ) (n : ℕ) : ℕ

The terminal degree used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.terminalDegree u n = MetricCodes.Hamming.longitudinalDegree u n

theorem MetricCodes.Johnson.Asymptotics.tendsto_shellWeight_ratio {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => ↑(shellWeight a n) / ↑n) Filter.atTop (nhds a)

theorem MetricCodes.Johnson.Asymptotics.tendsto_supportDegree_ratio {b : ℝ} (hb : 0 ≤ b) : Filter.Tendsto (fun (n : ℕ) => ↑(supportDegree b n) / ↑n) Filter.atTop (nhds b)

theorem MetricCodes.Johnson.Asymptotics.tendsto_complementDegree_ratio {g : ℝ} (hg : 0 ≤ g) : Filter.Tendsto (fun (n : ℕ) => ↑(complementDegree g n) / ↑n) Filter.atTop (nhds g)

theorem MetricCodes.Johnson.Asymptotics.tendsto_terminalDegree_ratio {u : ℝ} (hu : 0 ≤ u) : Filter.Tendsto (fun (n : ℕ) => ↑(terminalDegree u n) / ↑n) Filter.atTop (nhds u)

theorem MetricCodes.Johnson.Asymptotics.tendsto_dimension_ratio : Filter.Tendsto (fun (n : ℕ) => ↑n / ↑n) Filter.atTop (nhds 1)

theorem MetricCodes.Johnson.Asymptotics.tendsto_add_degree_ratio {f g : ℕ → ℕ} {a b : ℝ} (hf : Filter.Tendsto (fun (n : ℕ) => ↑(f n) / ↑n) Filter.atTop (nhds a)) (hg : Filter.Tendsto (fun (n : ℕ) => ↑(g n) / ↑n) Filter.atTop (nhds b)) : Filter.Tendsto (fun (n : ℕ) => ↑(f n + g n) / ↑n) Filter.atTop (nhds (a + b))

theorem MetricCodes.Johnson.Asymptotics.eventually_degree_lt_of_ratio {f g : ℕ → ℕ} {a b : ℝ} (hf : Filter.Tendsto (fun (n : ℕ) => ↑(f n) / ↑n) Filter.atTop (nhds a)) (hg : Filter.Tendsto (fun (n : ℕ) => ↑(g n) / ↑n) Filter.atTop (nhds b)) (hab : a < b) : ∀ᶠ (n : ℕ) in Filter.atTop, f n < g n

theorem MetricCodes.Johnson.Asymptotics.tendsto_atTop_of_ratio_pos {f : ℕ → ℕ} {a : ℝ} (ha : 0 < a) (hf : Filter.Tendsto (fun (n : ℕ) => ↑(f n) / ↑n) Filter.atTop (nhds a)) : Filter.Tendsto f Filter.atTop Filter.atTop

theorem MetricCodes.Johnson.Asymptotics.tendsto_sub_degree_ratio {f g : ℕ → ℕ} {a b : ℝ} (hf : Filter.Tendsto (fun (n : ℕ) => ↑(f n) / ↑n) Filter.atTop (nhds a)) (hg : Filter.Tendsto (fun (n : ℕ) => ↑(g n) / ↑n) Filter.atTop (nhds b)) (hgf : ∀ᶠ (n : ℕ) in Filter.atTop, g n ≤ f n) : Filter.Tendsto (fun (n : ℕ) => ↑(f n - g n) / ↑n) Filter.atTop (nhds (a - b))

theorem MetricCodes.Johnson.Asymptotics.scaled_binomialEntropy_identity {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hba : b < a) : (a * Real.log a - b * Real.log b - (a - b) * Real.log (a - b)) / Real.log 2 = a * binaryEntropy (b / a)

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_choose_of_ratio {N K : ℕ → ℕ} {a b : ℝ} (hN : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds a)) (hK : Filter.Tendsto (fun (n : ℕ) => ↑(K n) / ↑n) Filter.atTop (nhds b)) (hb : 0 < b) (hba : b < a) (hKN : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ N n) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑((N n).choose (K n)) / ↑n) Filter.atTop (nhds (a * binaryEntropy (b / a)))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_succ_of_le_dimension {N : ℕ → ℕ} (hN : ∀ᶠ (n : ℕ) in Filter.atTop, N n ≤ n) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(N n + 1) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_booleanHarmonicDimension_of_ratio {N K : ℕ → ℕ} {a b : ℝ} (hN : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds a)) (hK : Filter.Tendsto (fun (n : ℕ) => ↑(K n) / ↑n) Filter.atTop (nhds b)) (hb : 0 < b) (hba : b < a) (hhalf : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * K n ≤ N n) (hNle : ∀ᶠ (n : ℕ) in Filter.atTop, N n ≤ n) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(booleanHarmonicDimension (N n) (K n)) / ↑n) Filter.atTop (nhds (a * binaryEntropy (b / a)))

theorem MetricCodes.Johnson.Asymptotics.eventually_admissibleDegrees {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, AdmissibleDegrees n (shellWeight a n) (supportDegree b n) (complementDegree g n) (terminalDegree u n)

theorem MetricCodes.Johnson.Asymptotics.tendsto_complementShellWeight_ratio {a : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(n - shellWeight a n) / ↑n) Filter.atTop (nhds (1 - a))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_supportHarmonicDimension {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(booleanHarmonicDimension (shellWeight a n) (supportDegree b n)) / ↑n) Filter.atTop (nhds (a * binaryEntropy (b / a)))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_complementHarmonicDimension {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(booleanHarmonicDimension (n - shellWeight a n) (complementDegree g n)) / ↑n) Filter.atTop (nhds ((1 - a) * binaryEntropy (g / (1 - a))))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_johnsonFibreDimension {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(johnsonFibreDimension n (shellWeight a n) (supportDegree b n) (complementDegree g n)) / ↑n) Filter.atTop (nhds (rankPenalty a b g))

theorem MetricCodes.Johnson.Asymptotics.terminalHarmonic_le_johnsonAmbientDimension {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : booleanHarmonicDimension n L ≤ johnsonAmbientDimension n (p + q) L

theorem MetricCodes.Johnson.Asymptotics.johnsonAmbientDimension_le_terminalChoose {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) : johnsonAmbientDimension n (p + q) L ≤ n.choose L

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_johnsonAmbientDimension {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(johnsonAmbientDimension n (supportDegree b n + complementDegree g n) (terminalDegree u n)) / ↑n) Filter.atTop (nhds (binaryEntropy u))

noncomputable def MetricCodes.Johnson.Asymptotics.windowFibreQuotient (a b g u : ℝ) (n : ℕ) : ℝ

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

Equations

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

theorem MetricCodes.Johnson.Asymptotics.eventually_windowFibreQuotient_pos {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < windowFibreQuotient a b g u n

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_windowFibreQuotient {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (windowFibreQuotient a b g u n) / ↑n) Filter.atTop (nhds (binaryEntropy u - rankPenalty a b g))

noncomputable def MetricCodes.Johnson.Asymptotics.bassalygoFactor (a : ℝ) (n : ℕ) : ℝ

The bassalygo factor used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.bassalygoFactor a n = 2 ^ n / ↑(n.choose (MetricCodes.Johnson.Asymptotics.shellWeight a n))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_shellChoose {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 ↑(n.choose (shellWeight a n)) / ↑n) Filter.atTop (nhds (binaryEntropy a))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_bassalygoFactor {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (bassalygoFactor a n) / ↑n) Filter.atTop (nhds (1 - binaryEntropy a))

noncomputable def MetricCodes.Johnson.Asymptotics.bassalygoWindowFibreQuotient (a b g u : ℝ) (n : ℕ) : ℝ

The bassalygo window fibre quotient used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.Asymptotics.bassalygoWindowFibreQuotient a b g u n = MetricCodes.Johnson.Asymptotics.bassalygoFactor a n * MetricCodes.Johnson.Asymptotics.windowFibreQuotient a b g u n

theorem MetricCodes.Johnson.Asymptotics.eventually_bassalygoWindowFibreQuotient_pos {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < bassalygoWindowFibreQuotient a b g u n

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_bassalygoWindowFibreQuotient {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (bassalygoWindowFibreQuotient a b g u n) / ↑n) Filter.atTop (nhds (shellRate a b g u))

theorem MetricCodes.Johnson.Asymptotics.tendsto_logb_const_mul_bassalygoWindowFibreQuotient {d a b g u C : ℝ} (h : AsymptoticParameters d a b g u) (hC : 0 < C) : Filter.Tendsto (fun (n : ℕ) => Real.logb 2 (C * bassalygoWindowFibreQuotient a b g u n) / ↑n) Filter.atTop (nhds (shellRate a b g u))

theorem MetricCodes.Johnson.Asymptotics.centered_diagonal_limit_algebra {a m sigma eta z : ℝ} (hz : z ≠ 0) (hm : 1 - m ^ 2 ≠ 0) (hcenter : 1 - m ^ 2 = 4 * a * (1 - a)) : (m * sigma * eta / (4 * z ^ 2) - (m / 2) ^ 2) / (a * (1 - a)) = m * (sigma * eta - m * z ^ 2) / (z ^ 2 * (1 - m ^ 2))

theorem MetricCodes.Johnson.Asymptotics.tendsto_threshold_ceil {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : Filter.Tendsto (fun (n : ℕ) => threshold n (shellWeight a n) ⌈d * ↑n⌉₊) Filter.atTop (nhds (asymptoticThreshold d a))

theorem MetricCodes.Johnson.Asymptotics.binaryRate_le_shellRate_of_eventually {d a b g u C : ℝ} (h : AsymptoticParameters d a b g u) (hC : 0 < C) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Hamming.codeNumber n ⌈d * ↑n⌉₊) ≤ C * bassalygoWindowFibreQuotient a b g u n) : Hamming.binaryRate d ≤ shellRate a b g u

@[simp]

theorem MetricCodes.Johnson.coordinateSumEquiv_symm_support {n w : ℕ} (x : JohnsonSphere n w) (i : SupportCoordinates x) : (MetricCodes.Johnson.coordinateSumEquiv✝ x).symm ↑i = Sum.inl i

@[simp]

theorem MetricCodes.Johnson.coordinateSumEquiv_symm_complement {n w : ℕ} (x : JohnsonSphere n w) (i : ComplementCoordinates x) : (MetricCodes.Johnson.coordinateSumEquiv✝ x).symm ↑i = Sum.inr i

theorem MetricCodes.Johnson.coordinateSplitEquiv_card {n w : ℕ} (x : JohnsonSphere n w) (S : Finset (Fin n)) : ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1.card + ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2.card = S.card

theorem MetricCodes.Johnson.coordinateSplitEquiv_insert_support {n w : ℕ} (x : JohnsonSphere n w) (i : SupportCoordinates x) (S : Finset (Fin n)) : (MetricCodes.Johnson.coordinateSplitEquiv✝ x) (insert (↑i) S) = (insert i ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1, ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2)

theorem MetricCodes.Johnson.coordinateSplitEquiv_insert_complement {n w : ℕ} (x : JohnsonSphere n w) (i : ComplementCoordinates x) (S : Finset (Fin n)) : (MetricCodes.Johnson.coordinateSplitEquiv✝ x) (insert (↑i) S) = (((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1, insert i ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2)

theorem MetricCodes.Johnson.supportRaisedFunction_eq_zero_of_card_ne {n w p : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (a : Fin (hammingFibreDimension w p)) (r : ℕ) (S : Finset (SupportCoordinates x)) (hS : S.card ≠ p + r) : MetricCodes.Johnson.supportRaisedFunction✝ x hp a r S = 0

theorem MetricCodes.Johnson.complementRaisedFunction_eq_zero_of_card_ne {n w q : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (a : Fin (hammingFibreDimension (n - w) q)) (r : ℕ) (S : Finset (ComplementCoordinates x)) (hS : S.card ≠ q + r) : MetricCodes.Johnson.complementRaisedFunction✝ x hq a r S = 0

theorem MetricCodes.Johnson.supportRaisedFunction_pairing {n w p : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (a b : Fin (hammingFibreDimension w p)) (r s : ℕ) : ∑ S : Finset (SupportCoordinates x), MetricCodes.Johnson.supportRaisedFunction✝ x hp a r S * MetricCodes.Johnson.supportRaisedFunction✝ x hp b s S = Boolean.dot (Boolean.harmonicEmbedding p r (Boolean.harmonicBasisFunction w p hp a)) (Boolean.harmonicEmbedding p s (Boolean.harmonicBasisFunction w p hp b))

theorem MetricCodes.Johnson.complementRaisedFunction_pairing {n w q : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (a b : Fin (hammingFibreDimension (n - w) q)) (r s : ℕ) : ∑ S : Finset (ComplementCoordinates x), MetricCodes.Johnson.complementRaisedFunction✝ x hq a r S * MetricCodes.Johnson.complementRaisedFunction✝ x hq b s S = Boolean.dot (Boolean.harmonicEmbedding q r (Boolean.harmonicBasisFunction (n - w) q hq a)) (Boolean.harmonicEmbedding q s (Boolean.harmonicBasisFunction (n - w) q hq b))

theorem MetricCodes.Johnson.supportRaisedFunction_orthonormal {n w p r : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hr : 2 * p + r ≤ w) (a b : Fin (hammingFibreDimension w p)) : ∑ S : Finset (SupportCoordinates x), MetricCodes.Johnson.supportRaisedFunction✝ x hp a r S * MetricCodes.Johnson.supportRaisedFunction✝ x hp b r S = if a = b then 1 else 0

theorem MetricCodes.Johnson.complementRaisedFunction_orthonormal {n w q r : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (hr : 2 * q + r ≤ n - w) (a b : Fin (hammingFibreDimension (n - w) q)) : ∑ S : Finset (ComplementCoordinates x), MetricCodes.Johnson.complementRaisedFunction✝ x hq a r S * MetricCodes.Johnson.complementRaisedFunction✝ x hq b r S = if a = b then 1 else 0

theorem MetricCodes.Johnson.supportRaisedFunction_cross_orthogonal {n w p : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (a b : Fin (hammingFibreDimension w p)) (r s : ℕ) (hrs : r ≠ s) : ∑ S : Finset (SupportCoordinates x), MetricCodes.Johnson.supportRaisedFunction✝ x hp a r S * MetricCodes.Johnson.supportRaisedFunction✝ x hp b s S = 0

theorem MetricCodes.Johnson.splitTensor_isLevel {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (r s : ℕ) : Boolean.IsLevel (p + r + (q + s)) (MetricCodes.Johnson.splitTensor✝ x hp hq a r s)

theorem MetricCodes.Johnson.splitTensor_pairing {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a b : HarmonicFibreIndex n w p q) (r s r' s' : ℕ) : Boolean.dot (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) (MetricCodes.Johnson.splitTensor✝ x hp hq b r' s') = (∑ A : Finset (SupportCoordinates x), MetricCodes.Johnson.supportRaisedFunction✝ x hp a.1 r A * MetricCodes.Johnson.supportRaisedFunction✝ x hp b.1 r' A) * ∑ B : Finset (ComplementCoordinates x), MetricCodes.Johnson.complementRaisedFunction✝ x hq a.2 s B * MetricCodes.Johnson.complementRaisedFunction✝ x hq b.2 s' B

theorem MetricCodes.Johnson.splitTensor_orthonormal {n w p q r s : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hr : 2 * p + r ≤ w) (hs : 2 * q + s ≤ n - w) (a b : HarmonicFibreIndex n w p q) : Boolean.dot (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) (MetricCodes.Johnson.splitTensor✝ x hp hq b r s) = if a = b then 1 else 0

theorem MetricCodes.Johnson.splitTensor_cross_orthogonal {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a b : HarmonicFibreIndex n w p q) (r s r' s' : ℕ) (hrr' : r ≠ r') : Boolean.dot (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) (MetricCodes.Johnson.splitTensor✝ x hp hq b r' s') = 0

theorem MetricCodes.Johnson.clebschCoefficient_succ_mul {w N p q t r : ℕ} (hbound : 2 * p + (r + 1) ≤ w) : MetricCodes.Johnson.clebschCoefficient✝ w N p q t (r + 1) * √(Boolean.harmonicCoefficient w p (r + 1)) = -MetricCodes.Johnson.clebschCoefficient✝ w N p q t r * √(Boolean.harmonicCoefficient N q (t - r))

theorem MetricCodes.Johnson.clebschNormSq_pos (w N p q t : ℕ) : 0 < MetricCodes.Johnson.clebschNormSq✝ w N p q t

theorem MetricCodes.Johnson.coupledTensor_isLevel {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (t : ℕ) : Boolean.IsLevel (p + q + t) (MetricCodes.Johnson.coupledTensor✝ x hp hq a t)

noncomputable def MetricCodes.Johnson.coupledHarmonic {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (t : ℕ) : Boolean.Function n

The coupled harmonic used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.coupledHarmonic x hp hq a t = (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t))⁻¹ • MetricCodes.Johnson.coupledTensor✝ x hp hq a t

theorem MetricCodes.Johnson.coupledHarmonic_isLevel {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (t : ℕ) : Boolean.IsLevel (p + q + t) (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.dot_fintype_weighted_sum {n : ℕ} {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (c : ι → ℝ) (d : κ → ℝ) (f : ι → Boolean.Function n) (g : κ → Boolean.Function n) : (Boolean.dot (fun (S : Finset (Fin n)) => ∑ i : ι, c i * f i S) fun (S : Finset (Fin n)) => ∑ j : κ, d j * g j S) = ∑ i : ι, ∑ j : κ, c i * d j * Boolean.dot (f i) (g j)

theorem MetricCodes.Johnson.coupledTensor_dot {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a b : HarmonicFibreIndex n w p q) : Boolean.dot (MetricCodes.Johnson.coupledTensor✝ x hp hq a t) (MetricCodes.Johnson.coupledTensor✝ x hp hq b t) = MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t * if a = b then 1 else 0

theorem MetricCodes.Johnson.coupledHarmonic_dot {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a b : HarmonicFibreIndex n w p q) : Boolean.dot (coupledHarmonic x hp hq a t) (coupledHarmonic x hp hq b t) = if a = b then 1 else 0

@[simp]

theorem MetricCodes.Johnson.coordinateSplitEquiv_mem_support {n w : ℕ} (x : JohnsonSphere n w) (i : SupportCoordinates x) (S : Finset (Fin n)) : i ∈ ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1 ↔ ↑i ∈ S

@[simp]

theorem MetricCodes.Johnson.coordinateSplitEquiv_mem_complement {n w : ℕ} (x : JohnsonSphere n w) (i : ComplementCoordinates x) (S : Finset (Fin n)) : i ∈ ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2 ↔ ↑i ∈ S

theorem MetricCodes.Johnson.coordinateLower_reindex {m : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] (e : α ≃ Fin m) (f : Boolean.Function m) (S : Finset α) : MetricCodes.Johnson.coordinateLower✝ (fun (T : Finset α) => f (e.finsetCongr T)) S = Boolean.lower f (e.finsetCongr S)

theorem MetricCodes.Johnson.supportRaisedFunction_lower {n w p r : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hbound : 2 * p + (r + 1) ≤ w) (a : Fin (hammingFibreDimension w p)) (S : Finset (SupportCoordinates x)) : MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.supportRaisedFunction✝ x hp a (r + 1)) S = √(Boolean.harmonicCoefficient w p (r + 1)) * MetricCodes.Johnson.supportRaisedFunction✝ x hp a r S

theorem MetricCodes.Johnson.complementRaisedFunction_lower {n w q r : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (hbound : 2 * q + (r + 1) ≤ n - w) (a : Fin (hammingFibreDimension (n - w) q)) (S : Finset (ComplementCoordinates x)) : MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.complementRaisedFunction✝ x hq a (r + 1)) S = √(Boolean.harmonicCoefficient (n - w) q (r + 1)) * MetricCodes.Johnson.complementRaisedFunction✝ x hq a r S

theorem MetricCodes.Johnson.supportRaisedFunction_lower_zero {n w p : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (a : Fin (hammingFibreDimension w p)) (S : Finset (SupportCoordinates x)) : MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.supportRaisedFunction✝ x hp a 0) S = 0

theorem MetricCodes.Johnson.complementRaisedFunction_lower_zero {n w q : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (a : Fin (hammingFibreDimension (n - w) q)) (S : Finset (ComplementCoordinates x)) : MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.complementRaisedFunction✝ x hq a 0) S = 0

theorem MetricCodes.Johnson.lower_splitTensor {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (r s : ℕ) (S : Finset (Fin n)) : Boolean.lower (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) S = MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.supportRaisedFunction✝ x hp a.1 r) ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1 * MetricCodes.Johnson.complementRaisedFunction✝ x hq a.2 s ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2 + MetricCodes.Johnson.supportRaisedFunction✝ x hp a.1 r ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1 * MetricCodes.Johnson.coordinateLower✝ (MetricCodes.Johnson.complementRaisedFunction✝ x hq a.2 s) ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2

theorem MetricCodes.Johnson.lower_fintype_weighted_sum {n : ℕ} {ι : Type u_1} [Fintype ι] (c : ι → ℝ) (f : ι → Boolean.Function n) : (Boolean.lower fun (S : Finset (Fin n)) => ∑ i : ι, c i * f i S) = fun (S : Finset (Fin n)) => ∑ i : ι, c i * Boolean.lower (f i) S

theorem MetricCodes.Johnson.coupledTensor_lower_eq_zero {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) : Boolean.lower (MetricCodes.Johnson.coupledTensor✝ x hp hq a t) = 0

theorem MetricCodes.Johnson.coupledHarmonic_isHarmonic {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) : Boolean.IsHarmonic (p + q + t) (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.AdmissibleDegrees.supportResidual_bound {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (i : Index p q L) : 2 * p + ↑i ≤ w

theorem MetricCodes.Johnson.AdmissibleDegrees.complementResidual_bound {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (i : Index p q L) : 2 * q + ↑i ≤ n - w

theorem MetricCodes.Johnson.AdmissibleDegrees.window_degree_le_weight {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (i : Index p q L) : p + q + ↑i ≤ w

def MetricCodes.Johnson.globalHarmonicVector {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : ↥(Boolean.harmonicEuclideanLayer n j)

The global harmonic vector used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.globalHarmonicVector f hf = ⟨WithLp.toLp 2 (MetricCodes.Boolean.layerRestrict j f), ⋯⟩

theorem MetricCodes.Johnson.globalHarmonicVector_inner {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) : inner ℝ (globalHarmonicVector f hf) (globalHarmonicVector g hg) = Boolean.dot f g

theorem MetricCodes.Johnson.AdmissibleDegrees.window_degree_half {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (i : Index p q L) : 2 * (p + q + ↑i) ≤ n

noncomputable def MetricCodes.Johnson.coupledDegreeVector {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (x : JohnsonSphere n w) (i : Index p q L) (a : HarmonicFibreIndex n w p q) : ↥(Boolean.harmonicEuclideanLayer n (p + q + ↑i))

The coupled degree vector used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.coupledDegreeVector h x i a = MetricCodes.Johnson.globalHarmonicVector (MetricCodes.Johnson.coupledHarmonic x ⋯ ⋯ a ↑i) ⋯

noncomputable def MetricCodes.Johnson.coupledDegreeCoordinates {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (x : JohnsonSphere n w) (i : Index p q L) (a : HarmonicFibreIndex n w p q) (b : Fin (booleanHarmonicDimension n (p + q + ↑i))) : ℝ

The coupled degree coordinates used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.coupledDegreeCoordinates h x i a b = ((MetricCodes.Boolean.harmonicOrthonormalBasis n (p + q + ↑i) ⋯).repr (MetricCodes.Johnson.coupledDegreeVector h x i a)).ofLp b

theorem MetricCodes.Johnson.coupledDegreeCoordinates_pairing {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (x : JohnsonSphere n w) (i : Index p q L) (a b : HarmonicFibreIndex n w p q) : ∑ u : Fin (booleanHarmonicDimension n (p + q + ↑i)), coupledDegreeCoordinates h x i a u * coupledDegreeCoordinates h x i b u = if a = b then 1 else 0

noncomputable def MetricCodes.Johnson.johnsonWindowFibreMatrix {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (x : JohnsonSphere n w) : Matrix (ShellWindowIndex n p q L) (HarmonicFibreIndex n w p q) ℝ

The johnson window fibre matrix used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.johnsonWindowFibreMatrix h v x T a = MetricCodes.Johnson.johnsonFibreAmplitude n w p q L v T.fst * MetricCodes.Johnson.coupledDegreeCoordinates h x T.fst a T.snd

theorem MetricCodes.Johnson.johnsonWindowFibreMatrix_transpose_mul {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) (x : JohnsonSphere n w) : (johnsonWindowFibreMatrix h v x).transpose * johnsonWindowFibreMatrix h v x = 1

noncomputable def MetricCodes.Johnson.johnsonFibreMatrix {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (v : Space p q L) (x : JohnsonSphere n w) : Matrix (Fin (johnsonAmbientDimension n (p + q) L)) (Fin (johnsonFibreDimension n w p q)) ℝ

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

Equations

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

theorem MetricCodes.Johnson.johnsonFibreMatrix_transpose_mul {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) (x : JohnsonSphere n w) : (johnsonFibreMatrix h v x).transpose * johnsonFibreMatrix h v x = 1

noncomputable def MetricCodes.Johnson.johnsonProjectionFamily {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) : ProjectionFamily (JohnsonSphere n w) (johnsonAmbientDimension n (p + q) L) (johnsonFibreDimension n w p q)

The johnson projection family used in the Johnson-code argument.

Equations

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

theorem MetricCodes.Johnson.johnsonHarmonicGap_pos {n j : ℕ} (hj : 2 * j < n) : 0 < MetricCodes.Johnson.johnsonHarmonicGap✝ n j

theorem MetricCodes.Johnson.johnsonMiddleScale_pos {n j : ℕ} (hj : 0 < j) (hhalf : 2 * j < n) : 0 < MetricCodes.Johnson.johnsonMiddleScale✝ n j

theorem MetricCodes.Johnson.johnsonUpperScale_pos {n j : ℕ} (hhalf : 2 * (j + 1) ≤ n) : 0 < MetricCodes.Johnson.johnsonUpperScale✝ n j

theorem MetricCodes.Johnson.johnsonLowerAt_commutes {n : ℕ} (f : Boolean.Function n) (a : Fin n) : Boolean.lower (Boolean.lowerAt a f) = Boolean.lowerAt a (Boolean.lower f)

theorem MetricCodes.Johnson.johnsonLowerAt_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) (a : Fin n) : Boolean.IsHarmonic j (Boolean.lowerAt a f)

theorem MetricCodes.Johnson.johnsonLowerRaiseAt_commutator {n : ℕ} (f : Boolean.Function n) (a : Fin n) (S : Finset (Fin n)) : Boolean.lower (Boolean.raiseAt a f) S - Boolean.raiseAt a (Boolean.lower f) S = f S - 2 * Boolean.raiseAt a (Boolean.lowerAt a f) S

theorem MetricCodes.Johnson.johnsonLowerAt_lowerAt_self {n : ℕ} (f : Boolean.Function n) (a : Fin n) : Boolean.lowerAt a (Boolean.lowerAt a f) = 0

theorem MetricCodes.Johnson.johnsonLowerRaiseAtLowerAt_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin n) : Boolean.lower (Boolean.raiseAt a (Boolean.lowerAt a f)) = Boolean.lowerAt a f

theorem MetricCodes.Johnson.johnsonBooleanLower_sub {n : ℕ} (f g : Boolean.Function n) : Boolean.lower (f - g) = Boolean.lower f - Boolean.lower g

theorem MetricCodes.Johnson.johnsonMiddleRaw_isLevel {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hj : 0 < j) (a : Fin n) : Boolean.IsLevel j (MetricCodes.Johnson.johnsonMiddleRaw✝ j a f)

theorem MetricCodes.Johnson.johnsonMiddleRaw_isHarmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hj : 0 < j) (hhalf : 2 * j < n) (a : Fin n) : Boolean.IsHarmonic j (MetricCodes.Johnson.johnsonMiddleRaw✝ j a f)

theorem MetricCodes.Johnson.johnsonLowerAt_eq_zero_of_level_zero {n : ℕ} (f : Boolean.Function n) (hf : Boolean.IsLevel 0 f) (a : Fin n) : Boolean.lowerAt a f = 0

theorem MetricCodes.Johnson.johnsonMembership_isLevel {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsLevel j f) (a : Fin n) : Boolean.IsLevel j (Boolean.raiseAt a (Boolean.lowerAt a f))

theorem MetricCodes.Johnson.johnsonUpperRaw_isLevel {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin n) : Boolean.IsLevel (j + 1) (MetricCodes.Johnson.johnsonUpperRaw✝ j a f)

theorem MetricCodes.Johnson.johnsonLowerRaise_of_level {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsLevel j f) : Boolean.lower (Boolean.raise f) = Boolean.raise (Boolean.lower f) + MetricCodes.Johnson.johnsonHarmonicGap✝ n j • f

theorem MetricCodes.Johnson.johnsonLowerRaiseAt_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin n) : Boolean.lower (Boolean.raiseAt a f) = f - 2 • Boolean.raiseAt a (Boolean.lowerAt a f)

theorem MetricCodes.Johnson.johnsonLowerRaise_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : Boolean.lower (Boolean.raise f) = MetricCodes.Johnson.johnsonHarmonicGap✝ n j • f

theorem MetricCodes.Johnson.johnsonLowerDoubleRaiseLowerAt_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin n) : Boolean.lower (Boolean.raise (Boolean.raise (Boolean.lowerAt a f))) = (2 * (MetricCodes.Johnson.johnsonHarmonicGap✝ n j + 1)) • Boolean.raise (Boolean.lowerAt a f)

theorem MetricCodes.Johnson.johnsonLowerRaiseMembership_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin n) : Boolean.lower (Boolean.raise (Boolean.raiseAt a (Boolean.lowerAt a f))) = Boolean.raise (Boolean.lowerAt a f) + MetricCodes.Johnson.johnsonHarmonicGap✝ n j • Boolean.raiseAt a (Boolean.lowerAt a f)

theorem MetricCodes.Johnson.johnsonUpperRaw_isHarmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hhalf : 2 * (j + 1) ≤ n) (a : Fin n) : Boolean.IsHarmonic (j + 1) (MetricCodes.Johnson.johnsonUpperRaw✝ j a f)

theorem MetricCodes.Johnson.johnsonBooleanDot_sub_left {n : ℕ} (f g h : Boolean.Function n) : Boolean.dot (f - g) h = Boolean.dot f h - Boolean.dot g h

theorem MetricCodes.Johnson.johnsonBooleanDot_sub_right {n : ℕ} (f g h : Boolean.Function n) : Boolean.dot f (g - h) = Boolean.dot f g - Boolean.dot f h

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

theorem MetricCodes.Johnson.johnsonDotRaise_harmonic_right {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic j g) : Boolean.dot (Boolean.raise f) g = 0

theorem MetricCodes.Johnson.johnsonLowerAtRaiseAtLowerAt {n : ℕ} (f : Boolean.Function n) (a : Fin n) : Boolean.lowerAt a (Boolean.raiseAt a (Boolean.lowerAt a f)) = Boolean.lowerAt a f

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

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

theorem MetricCodes.Johnson.johnsonSumDotMembershipRight {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsLevel j g) : ∑ a : Fin n, Boolean.dot f (Boolean.raiseAt a (Boolean.lowerAt a g)) = ↑j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonLowerRaiseLowerAt_of_harmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hj : 0 < j) (a : Fin n) : Boolean.lower (Boolean.raise (Boolean.lowerAt a f)) = (MetricCodes.Johnson.johnsonHarmonicGap✝ n j + 2) • Boolean.lowerAt a f

theorem MetricCodes.Johnson.johnsonSumDotMembershipRaisedDeletion {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : ∑ a : Fin n, Boolean.dot (Boolean.raiseAt a (Boolean.lowerAt a f)) (Boolean.raise (Boolean.lowerAt a g)) = ↑j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonSumDotRaisedDeletionMembership {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsLevel j f) (hg : Boolean.IsHarmonic j g) : ∑ a : Fin n, Boolean.dot (Boolean.raise (Boolean.lowerAt a f)) (Boolean.raiseAt a (Boolean.lowerAt a g)) = ↑j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonSumDotRaisedDeletionRaisedDeletion {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsLevel j f) (hg : Boolean.IsHarmonic j g) (hj : 0 < j) : ∑ a : Fin n, Boolean.dot (Boolean.raise (Boolean.lowerAt a f)) (Boolean.raise (Boolean.lowerAt a g)) = (MetricCodes.Johnson.johnsonHarmonicGap✝ n j + 2) * (↑j * Boolean.dot f g)

theorem MetricCodes.Johnson.johnsonSumDotRaisedDeletionHarmonicRight {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic j g) : ∑ a : Fin n, Boolean.dot (Boolean.raise (Boolean.lowerAt a f)) g = 0

theorem MetricCodes.Johnson.johnsonSumDotHarmonicRaisedDeletion {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : ∑ a : Fin n, Boolean.dot f (Boolean.raise (Boolean.lowerAt a g)) = 0

theorem MetricCodes.Johnson.johnsonMiddleRaw_coordinateDot {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) (hj : 0 < j) (hhalf : 2 * j < n) : (Boolean.coordinateDot (fun (a : Fin n) => MetricCodes.Johnson.johnsonMiddleRaw✝ j a f) fun (a : Fin n) => MetricCodes.Johnson.johnsonMiddleRaw✝ j a g) = MetricCodes.Johnson.johnsonMiddleScale✝ n j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonMiddleChannel_isometry {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) (hj : 0 < j) (hhalf : 2 * j < n) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonMiddleChannel✝ j f) (MetricCodes.Johnson.johnsonMiddleChannel✝ j g) = Boolean.dot f g

theorem MetricCodes.Johnson.johnsonSumDotRaiseAtRaise {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic j g) : ∑ a : Fin n, Boolean.dot (Boolean.raiseAt a f) (Boolean.raise g) = MetricCodes.Johnson.johnsonHarmonicGap✝ n j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonSumDotRaiseAtRaisedMembership {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsLevel j g) : ∑ a : Fin n, Boolean.dot (Boolean.raiseAt a f) (Boolean.raise (Boolean.raiseAt a (Boolean.lowerAt a g))) = -↑j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonSumDotRaiseAtDoubleRaisedDeletion {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : ∑ a : Fin n, Boolean.dot (Boolean.raiseAt a f) (Boolean.raise (Boolean.raise (Boolean.lowerAt a g))) = -(2 * ↑j) * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonUpperRaw_dot_eq_coordinateCreation {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic j g) (hhalf : 2 * (j + 1) ≤ n) (a : Fin n) : Boolean.dot (MetricCodes.Johnson.johnsonUpperRaw✝ j a f) (MetricCodes.Johnson.johnsonUpperRaw✝ j a g) = Boolean.dot (Boolean.raiseAt a f) (MetricCodes.Johnson.johnsonUpperRaw✝ j a g)

theorem MetricCodes.Johnson.johnsonUpperRaw_coordinateDot {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) (hhalf : 2 * (j + 1) ≤ n) : (Boolean.coordinateDot (fun (a : Fin n) => MetricCodes.Johnson.johnsonUpperRaw✝ j a f) fun (a : Fin n) => MetricCodes.Johnson.johnsonUpperRaw✝ j a g) = MetricCodes.Johnson.johnsonUpperScale✝ n j * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonUpperChannel_isometry {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) (hhalf : 2 * (j + 1) ≤ n) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonUpperChannel✝ j f) (MetricCodes.Johnson.johnsonUpperChannel✝ j g) = Boolean.dot f g

theorem MetricCodes.Johnson.johnsonLowerChannel_isometry {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hj : 0 < j) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonLowerChannel✝ j f) (MetricCodes.Johnson.johnsonLowerChannel✝ j g) = Boolean.dot f g

theorem MetricCodes.Johnson.johnsonDotHarmonicRaise {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : Boolean.dot f (Boolean.raise g) = 0

theorem MetricCodes.Johnson.johnsonSumDotRaiseAtRight {n : ℕ} (f g : Boolean.Function n) : ∑ a : Fin n, Boolean.dot f (Boolean.raiseAt a g) = Boolean.dot f (Boolean.raise g)

theorem MetricCodes.Johnson.johnsonSumDotLowerAtRight {n : ℕ} (f g : Boolean.Function n) : ∑ a : Fin n, Boolean.dot (Boolean.lowerAt a f) g = Boolean.dot f (Boolean.raise g)

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

theorem MetricCodes.Johnson.johnsonDotRaisedDeletionRaiseAt {n j : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic j g) (a : Fin n) : Boolean.dot (Boolean.raise (Boolean.lowerAt a f)) (Boolean.raiseAt a g) = Boolean.dot (Boolean.lowerAt a f) g

theorem MetricCodes.Johnson.johnsonLowerMiddleRaw_orthogonal {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) : (Boolean.coordinateDot (fun (a : Fin n) => Boolean.lowerAt a f) fun (a : Fin n) => MetricCodes.Johnson.johnsonMiddleRaw✝ j a g) = 0

theorem MetricCodes.Johnson.johnsonLowerUpperRaw_orthogonal {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 2) f) : (Boolean.coordinateDot (fun (a : Fin n) => Boolean.lowerAt a f) fun (a : Fin n) => MetricCodes.Johnson.johnsonUpperRaw✝ j a g) = 0

theorem MetricCodes.Johnson.johnsonMiddleUpperRaw_orthogonal {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) (hg : Boolean.IsHarmonic j g) (hhalf : 2 * (j + 1) < n) : (Boolean.coordinateDot (fun (a : Fin n) => MetricCodes.Johnson.johnsonMiddleRaw✝ (j + 1) a f) fun (a : Fin n) => MetricCodes.Johnson.johnsonUpperRaw✝ j a g) = 0

theorem MetricCodes.Johnson.johnsonCoordinateDot_smul {n : ℕ} (c d : ℝ) (f g : Boolean.CoordinateFunction n) : (Boolean.coordinateDot (fun (a : Fin n) => c • f a) fun (a : Fin n) => d • g a) = c * d * Boolean.coordinateDot f g

theorem MetricCodes.Johnson.johnsonLowerChannel_orthogonal_middleChannel {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonLowerChannel✝ (j + 1) f) (MetricCodes.Johnson.johnsonMiddleChannel✝ j g) = 0

theorem MetricCodes.Johnson.johnsonLowerChannel_orthogonal_upperChannel {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 2) f) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonLowerChannel✝ (j + 2) f) (MetricCodes.Johnson.johnsonUpperChannel✝ j g) = 0

theorem MetricCodes.Johnson.johnsonMiddleChannel_orthogonal_upperChannel {n j : ℕ} (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) (hg : Boolean.IsHarmonic j g) (hhalf : 2 * (j + 1) < n) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonMiddleChannel✝ (j + 1) f) (MetricCodes.Johnson.johnsonUpperChannel✝ j g) = 0

theorem MetricCodes.Johnson.johnsonHarmonic_smul {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (c : ℝ) : Boolean.IsHarmonic j (c • f)

theorem MetricCodes.Johnson.johnsonLowerChannel_isHarmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic (j + 1) f) (a : Fin n) : Boolean.IsHarmonic j (MetricCodes.Johnson.johnsonLowerChannel✝ (j + 1) f a)

theorem MetricCodes.Johnson.johnsonMiddleChannel_isHarmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hhalf : 2 * j < n) (a : Fin n) : Boolean.IsHarmonic j (MetricCodes.Johnson.johnsonMiddleChannel✝ j f a)

theorem MetricCodes.Johnson.johnsonUpperChannel_isHarmonic {n j : ℕ} (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hhalf : 2 * (j + 1) ≤ n) (a : Fin n) : Boolean.IsHarmonic (j + 1) (MetricCodes.Johnson.johnsonUpperChannel✝ j f a)

theorem MetricCodes.Johnson.johnsonDiagonalChannelSign_sq (n w p q j : ℕ) : MetricCodes.Johnson.johnsonDiagonalChannelSign✝ n w p q j ^ 2 = 1

noncomputable def MetricCodes.Johnson.johnsonAdjacentChannel (n w p q L : ℕ) (target source : Index p q L) (f : Boolean.Function n) : Boolean.CoordinateFunction n

The johnson adjacent channel used in the Johnson-code argument.

Equations

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

def MetricCodes.Johnson.johnsonChannelActive (p q L : ℕ) (target source : Index p q L) : Prop

The johnson channel active used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.johnsonChannelActive p q L target source = (↑target + 1 = ↑source ∨ target = source ∧ 0 < p + q + ↑source ∨ ↑source + 1 = ↑target)

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_eq_zero_of_not_active {n w p q L : ℕ} (source target : Index p q L) (hinactive : ¬johnsonChannelActive p q L target source) : johnsonSourceChannelCoefficient n w p q L source target = 0

theorem MetricCodes.Johnson.johnsonZero_isHarmonic (n j : ℕ) : Boolean.IsHarmonic j 0

theorem MetricCodes.Johnson.johnsonMiddleChannel_zero_degree {n : ℕ} (f : Boolean.Function n) : MetricCodes.Johnson.johnsonMiddleChannel✝ 0 f = 0

theorem MetricCodes.Johnson.johnsonAdjacentChannel_eq_zero_of_not_active {n w p q L : ℕ} (target source : Index p q L) (f : Boolean.Function n) (hinactive : ¬johnsonChannelActive p q L target source) : johnsonAdjacentChannel n w p q L target source f = 0

theorem MetricCodes.Johnson.johnsonCoordinateDot_pi_smul {n : ℕ} (c d : ℝ) (f g : Boolean.CoordinateFunction n) : Boolean.coordinateDot (c • f) (d • g) = c * d * Boolean.coordinateDot f g

theorem MetricCodes.Johnson.johnsonAdjacentChannel_isHarmonic {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (a : Fin n) : Boolean.IsHarmonic (p + q + ↑target) (johnsonAdjacentChannel n w p q L target source f a)

theorem MetricCodes.Johnson.johnsonAdjacentChannel_isometry {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hactive : johnsonChannelActive p q L target source) (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (hg : Boolean.IsHarmonic (p + q + ↑source) g) : Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target source f) (johnsonAdjacentChannel n w p q L target source g) = Boolean.dot f g

theorem MetricCodes.Johnson.johnsonAdjacentChannel_orthogonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source other : Index p q L) (hne : source ≠ other) (f g : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (hg : Boolean.IsHarmonic (p + q + ↑other) g) : Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target source f) (johnsonAdjacentChannel n w p q L target other g) = 0

noncomputable def MetricCodes.Johnson.johnsonAxisTensor {n w : ℕ} (x : JohnsonSphere n w) (f : Boolean.Function n) : Boolean.CoordinateFunction n

The johnson axis tensor used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.johnsonAxisTensor x f a = (MetricCodes.Johnson.geometricAxis x).ofLp a • f

theorem MetricCodes.Johnson.sum_geometricAxis {n w : ℕ} (hn : 0 < n) (x : JohnsonSphere n w) : ∑ a : Fin n, (geometricAxis x).ofLp a = 0

theorem MetricCodes.Johnson.johnsonDot_axisRaise {n w : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisRaise✝ x g) = ∑ a : Fin n, (geometricAxis x).ofLp a * Boolean.dot f (Boolean.raiseAt a g)

theorem MetricCodes.Johnson.johnsonDot_axisLower {n w : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisLower✝ x g) = ∑ a : Fin n, (geometricAxis x).ofLp a * Boolean.dot f (Boolean.lowerAt a g)

theorem MetricCodes.Johnson.johnsonDot_axisMembership {n w : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisMembership✝ x g) = ∑ a : Fin n, (geometricAxis x).ofLp a * Boolean.dot f (Boolean.raiseAt a (Boolean.lowerAt a g))

theorem MetricCodes.Johnson.johnsonLowerChannel_axis_inner {n w j : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonLowerChannel✝ j f) (johnsonAxisTensor x g) = (√↑j)⁻¹ * Boolean.dot f (MetricCodes.Johnson.johnsonAxisRaise✝ x g)

theorem MetricCodes.Johnson.johnsonUpperRaw_dot_harmonic_right {n j k : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic k g) (a : Fin n) : Boolean.dot (MetricCodes.Johnson.johnsonUpperRaw✝ j a f) g = Boolean.dot (Boolean.raiseAt a f) g

theorem MetricCodes.Johnson.johnsonUpperChannel_axis_inner {n w j k : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) (hg : Boolean.IsHarmonic k g) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonUpperChannel✝ j f) (johnsonAxisTensor x g) = (√(MetricCodes.Johnson.johnsonUpperScale✝ n j))⁻¹ * Boolean.dot f (MetricCodes.Johnson.johnsonAxisLower✝ x g)

theorem MetricCodes.Johnson.johnsonMiddleRaw_dot_harmonic_right {n j k : ℕ} (f g : Boolean.Function n) (hg : Boolean.IsHarmonic k g) (a : Fin n) : Boolean.dot (MetricCodes.Johnson.johnsonMiddleRaw✝ j a f) g = Boolean.dot f (Boolean.raiseAt a (Boolean.lowerAt a g)) - ↑j / ↑n * Boolean.dot f g

theorem MetricCodes.Johnson.johnsonMiddleChannel_axis_inner {n w j k : ℕ} (hn : 0 < n) (x : JohnsonSphere n w) (f g : Boolean.Function n) (hg : Boolean.IsHarmonic k g) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonMiddleChannel✝ j f) (johnsonAxisTensor x g) = (√(MetricCodes.Johnson.johnsonMiddleScale✝ n j))⁻¹ * Boolean.dot f (MetricCodes.Johnson.johnsonAxisMembership✝ x g)

theorem MetricCodes.Johnson.sum_coordinateIndicator_on_subset {n w : ℕ} (x : JohnsonSphere n w) (S : Finset (Fin n)) : (∑ a : Fin n, if a ∈ S then coordinateIndicator (↑x) a else 0) = ↑((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1.card

theorem MetricCodes.Johnson.sum_geometricAxis_on_subset {n w : ℕ} (x : JohnsonSphere n w) (S : Finset (Fin n)) : (∑ a : Fin n, if a ∈ S then (geometricAxis x).ofLp a else 0) = √(↑n / (↑w * ↑(n - w))) * (↑((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1.card - ↑w / ↑n * ↑S.card)

theorem MetricCodes.Johnson.johnsonAxisMembership_apply {n w : ℕ} (x : JohnsonSphere n w) (f : Boolean.Function n) (S : Finset (Fin n)) : MetricCodes.Johnson.johnsonAxisMembership✝ x f S = (∑ a : Fin n, if a ∈ S then (geometricAxis x).ofLp a else 0) * f S

theorem MetricCodes.Johnson.johnsonAxisMembership_splitTensor {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (r s : ℕ) : MetricCodes.Johnson.johnsonAxisMembership✝ x (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) = (√(↑n / (↑w * ↑(n - w))) * (↑(p + r) - ↑w / ↑n * ↑(p + r + (q + s)))) • MetricCodes.Johnson.splitTensor✝ x hp hq a r s

theorem MetricCodes.Johnson.johnsonAxisMembership_smul {n w : ℕ} (x : JohnsonSphere n w) (c : ℝ) (f : Boolean.Function n) : MetricCodes.Johnson.johnsonAxisMembership✝ x (c • f) = c • MetricCodes.Johnson.johnsonAxisMembership✝ x f

theorem MetricCodes.Johnson.johnsonDot_fintype_weighted_sum_right {n : ℕ} {ι : Type u_1} [Fintype ι] (f : Boolean.Function n) (c : ι → ℝ) (g : ι → Boolean.Function n) : (Boolean.dot f fun (S : Finset (Fin n)) => ∑ i : ι, c i * g i S) = ∑ i : ι, c i * Boolean.dot f (g i)

theorem MetricCodes.Johnson.johnsonAxisMembership_coupledTensor {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (t : ℕ) : MetricCodes.Johnson.johnsonAxisMembership✝ x (MetricCodes.Johnson.coupledTensor✝ x hp hq a t) = fun (S : Finset (Fin n)) => ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * (√(↑n / (↑w * ↑(n - w))) * (↑(p + ↑r) - ↑w / ↑n * ↑(p + q + t))) * MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r) S

theorem MetricCodes.Johnson.johnsonAxisMembership_coupledHarmonic_dot {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (t : ℕ) (f : Boolean.Function n) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisMembership✝ x (coupledHarmonic x hp hq a t)) = (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t))⁻¹ * √(↑n / (↑w * ↑(n - w))) * ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * (↑(p + ↑r) - ↑w / ↑n * ↑(p + q + t)) * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r))

theorem MetricCodes.Johnson.coordinateSplitEquiv_erase_support {n w : ℕ} (x : JohnsonSphere n w) (i : SupportCoordinates x) (S : Finset (Fin n)) : (MetricCodes.Johnson.coordinateSplitEquiv✝ x) (S.erase ↑i) = (((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1.erase i, ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2)

theorem MetricCodes.Johnson.coordinateSplitEquiv_erase_complement {n w : ℕ} (x : JohnsonSphere n w) (i : ComplementCoordinates x) (S : Finset (Fin n)) : (MetricCodes.Johnson.coordinateSplitEquiv✝ x) (S.erase ↑i) = (((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1, ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2.erase i)

theorem MetricCodes.Johnson.coordinateRaise_reindex {m : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] (e : α ≃ Fin m) (f : Boolean.Function m) (S : Finset α) : MetricCodes.Johnson.coordinateRaise✝ (fun (T : Finset α) => f (e.finsetCongr T)) S = Boolean.raise f (e.finsetCongr S)

theorem MetricCodes.Johnson.supportRaisedFunction_raise {n w p r : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hbound : 2 * p + (r + 1) ≤ w) (a : Fin (hammingFibreDimension w p)) (S : Finset (SupportCoordinates x)) : MetricCodes.Johnson.coordinateRaise✝ (MetricCodes.Johnson.supportRaisedFunction✝ x hp a r) S = √(Boolean.harmonicCoefficient w p (r + 1)) * MetricCodes.Johnson.supportRaisedFunction✝ x hp a (r + 1) S

theorem MetricCodes.Johnson.complementRaisedFunction_raise {n w q r : ℕ} (x : JohnsonSphere n w) (hq : 2 * q ≤ n - w) (hbound : 2 * q + (r + 1) ≤ n - w) (a : Fin (hammingFibreDimension (n - w) q)) (S : Finset (ComplementCoordinates x)) : MetricCodes.Johnson.coordinateRaise✝ (MetricCodes.Johnson.complementRaisedFunction✝ x hq a r) S = √(Boolean.harmonicCoefficient (n - w) q (r + 1)) * MetricCodes.Johnson.complementRaisedFunction✝ x hq a (r + 1) S

theorem MetricCodes.Johnson.raise_splitTensor {n w p q : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (r s : ℕ) (S : Finset (Fin n)) : Boolean.raise (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) S = MetricCodes.Johnson.coordinateRaise✝ (MetricCodes.Johnson.supportRaisedFunction✝ x hp a.1 r) ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1 * MetricCodes.Johnson.complementRaisedFunction✝ x hq a.2 s ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2 + MetricCodes.Johnson.supportRaisedFunction✝ x hp a.1 r ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).1 * MetricCodes.Johnson.coordinateRaise✝ (MetricCodes.Johnson.complementRaisedFunction✝ x hq a.2 s) ((MetricCodes.Johnson.coordinateSplitEquiv✝ x) S).2

theorem MetricCodes.Johnson.raise_splitTensor_eq {n w p q r s : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hsupport : 2 * p + (r + 1) ≤ w) (hcomplement : 2 * q + (s + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) : Boolean.raise (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) = √(Boolean.harmonicCoefficient w p (r + 1)) • MetricCodes.Johnson.splitTensor✝ x hp hq a (r + 1) s + √(Boolean.harmonicCoefficient (n - w) q (s + 1)) • MetricCodes.Johnson.splitTensor✝ x hp hq a r (s + 1)

theorem MetricCodes.Johnson.johnsonHarmonic_dot_splitTensor_succ_mul {n w p q t r : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) (hr : r < t) : √(Boolean.harmonicCoefficient w p (r + 1)) * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a (r + 1) (t - (r + 1))) = -√(Boolean.harmonicCoefficient (n - w) q (t - r)) * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a r (t - r))

theorem MetricCodes.Johnson.johnsonHarmonic_dot_splitTensor_eq_clebschCoefficient {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) (r : ℕ) (hr : r ≤ t) : Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a r (t - r)) = MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t r * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)

theorem MetricCodes.Johnson.johnsonHarmonic_dot_coupledHarmonic {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) : Boolean.dot f (coupledHarmonic x hp hq a t) = √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)

theorem MetricCodes.Johnson.sum_coordinateIndicator_mul_function {n w : ℕ} (x : JohnsonSphere n w) (F : Fin n → ℝ) : ∑ i : Fin n, coordinateIndicator (↑x) i * F i = ∑ i : SupportCoordinates x, F ↑i

theorem MetricCodes.Johnson.johnsonAxisRaise_eq_support {n w : ℕ} (x : JohnsonSphere n w) (f : Boolean.Function n) : MetricCodes.Johnson.johnsonAxisRaise✝ x f = √(↑n / (↑w * ↑(n - w))) • (MetricCodes.Johnson.johnsonSupportRaise✝ x f - (↑w / ↑n) • Boolean.raise f)

theorem MetricCodes.Johnson.johnsonAxisLower_eq_support {n w : ℕ} (x : JohnsonSphere n w) (f : Boolean.Function n) : MetricCodes.Johnson.johnsonAxisLower✝ x f = √(↑n / (↑w * ↑(n - w))) • (MetricCodes.Johnson.johnsonSupportLower✝ x f - (↑w / ↑n) • Boolean.lower f)

theorem MetricCodes.Johnson.johnsonAxisRaise_dot_harmonic_left {n w j : ℕ} (x : JohnsonSphere n w) (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisRaise✝ x g) = √(↑n / (↑w * ↑(n - w))) * Boolean.dot f (MetricCodes.Johnson.johnsonSupportRaise✝ x g)

theorem MetricCodes.Johnson.johnsonAxisLower_eq_support_of_harmonic {n w j : ℕ} (x : JohnsonSphere n w) (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) : MetricCodes.Johnson.johnsonAxisLower✝ x f = √(↑n / (↑w * ↑(n - w))) • MetricCodes.Johnson.johnsonSupportLower✝ x f

theorem MetricCodes.Johnson.johnsonSupportRaise_smul {n w : ℕ} (x : JohnsonSphere n w) (c : ℝ) (f : Boolean.Function n) : MetricCodes.Johnson.johnsonSupportRaise✝ x (c • f) = c • MetricCodes.Johnson.johnsonSupportRaise✝ x f

theorem MetricCodes.Johnson.johnsonSupportLower_smul {n w : ℕ} (x : JohnsonSphere n w) (c : ℝ) (f : Boolean.Function n) : MetricCodes.Johnson.johnsonSupportLower✝ x (c • f) = c • MetricCodes.Johnson.johnsonSupportLower✝ x f

theorem MetricCodes.Johnson.johnsonSupportRaise_fintype_weighted_sum {n w : ℕ} {ι : Type u_1} [Fintype ι] (x : JohnsonSphere n w) (c : ι → ℝ) (f : ι → Boolean.Function n) : (MetricCodes.Johnson.johnsonSupportRaise✝ x fun (S : Finset (Fin n)) => ∑ i : ι, c i * f i S) = fun (S : Finset (Fin n)) => ∑ i : ι, c i * MetricCodes.Johnson.johnsonSupportRaise✝ x (f i) S

theorem MetricCodes.Johnson.johnsonSupportLower_fintype_weighted_sum {n w : ℕ} {ι : Type u_1} [Fintype ι] (x : JohnsonSphere n w) (c : ι → ℝ) (f : ι → Boolean.Function n) : (MetricCodes.Johnson.johnsonSupportLower✝ x fun (S : Finset (Fin n)) => ∑ i : ι, c i * f i S) = fun (S : Finset (Fin n)) => ∑ i : ι, c i * MetricCodes.Johnson.johnsonSupportLower✝ x (f i) S

theorem MetricCodes.Johnson.johnsonSupportRaise_splitTensor {n w p q r s : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hsupport : 2 * p + (r + 1) ≤ w) (a : HarmonicFibreIndex n w p q) : MetricCodes.Johnson.johnsonSupportRaise✝ x (MetricCodes.Johnson.splitTensor✝ x hp hq a r s) = √(Boolean.harmonicCoefficient w p (r + 1)) • MetricCodes.Johnson.splitTensor✝ x hp hq a (r + 1) s

theorem MetricCodes.Johnson.johnsonSupportLower_splitTensor_succ {n w p q r s : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hsupport : 2 * p + (r + 1) ≤ w) (a : HarmonicFibreIndex n w p q) : MetricCodes.Johnson.johnsonSupportLower✝ x (MetricCodes.Johnson.splitTensor✝ x hp hq a (r + 1) s) = √(Boolean.harmonicCoefficient w p (r + 1)) • MetricCodes.Johnson.splitTensor✝ x hp hq a r s

theorem MetricCodes.Johnson.johnsonSupportLower_splitTensor_zero {n w p q s : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) : MetricCodes.Johnson.johnsonSupportLower✝ x (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 s) = 0

theorem MetricCodes.Johnson.johnsonSupportRaise_coupledTensor {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hsupport : 2 * p + (t + 1) ≤ w) (a : HarmonicFibreIndex n w p q) : MetricCodes.Johnson.johnsonSupportRaise✝ x (MetricCodes.Johnson.coupledTensor✝ x hp hq a t) = fun (S : Finset (Fin n)) => ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r + 1) (t - ↑r) S

theorem MetricCodes.Johnson.johnsonSupportLower_coupledTensor_succ {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (hsupport : 2 * p + (t + 1) ≤ w) (a : HarmonicFibreIndex n w p q) : MetricCodes.Johnson.johnsonSupportLower✝ x (MetricCodes.Johnson.coupledTensor✝ x hp hq a (t + 1)) = fun (S : Finset (Fin n)) => ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q (t + 1) (↑r + 1) * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r) S

theorem MetricCodes.Johnson.johnsonAxisRaise_coupledHarmonic_dot {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + (t + 1)) f) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisRaise✝ x (coupledHarmonic x hp hq a t)) = (√(↑n / (↑w * ↑(n - w))) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t))⁻¹ * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1)))⁻¹ * ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q (t + 1) (↑r + 1)) * Boolean.dot f (coupledHarmonic x hp hq a (t + 1))

theorem MetricCodes.Johnson.johnsonAxisLower_coupledHarmonic_dot {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisLower✝ x (coupledHarmonic x hp hq a (t + 1))) = (√(↑n / (↑w * ↑(n - w))) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1)))⁻¹ * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t))⁻¹ * ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q (t + 1) (↑r + 1) * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.clebschCoefficient_sq_succ_mul {w N p q t r : ℕ} (hsupport : 2 * p + (r + 1) ≤ w) (hcomplement : 2 * q + t ≤ N) : MetricCodes.Johnson.clebschCoefficient✝ w N p q t (r + 1) ^ 2 * Boolean.harmonicCoefficient w p (r + 1) = MetricCodes.Johnson.clebschCoefficient✝ w N p q t r ^ 2 * Boolean.harmonicCoefficient N q (t - r)

theorem MetricCodes.Johnson.clebschCoefficient_sq_harmonic_balance {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient w p ↑r = ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient N q (t - ↑r)

theorem MetricCodes.Johnson.clebsch_support_moment_expansion (w N p q t : ℕ) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient w p ↑r = (↑w - 2 * ↑p + 1) * MetricCodes.Johnson.clebschFirstMoment✝ w N p q t - MetricCodes.Johnson.clebschSecondMoment✝ w N p q t

theorem MetricCodes.Johnson.clebsch_complement_moment_expansion (w N p q t : ℕ) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient N q (t - ↑r) = ↑t * (↑N - 2 * ↑q - ↑t + 1) * MetricCodes.Johnson.clebschNormSq✝ w N p q t + (2 * ↑t - (↑N - 2 * ↑q) - 1) * MetricCodes.Johnson.clebschFirstMoment✝ w N p q t - MetricCodes.Johnson.clebschSecondMoment✝ w N p q t

theorem MetricCodes.Johnson.clebschFirstMoment_mul {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) : (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 2) * MetricCodes.Johnson.clebschFirstMoment✝ w N p q t = ↑t * (↑N - 2 * ↑q - ↑t + 1) * MetricCodes.Johnson.clebschNormSq✝ w N p q t

theorem MetricCodes.Johnson.clebschFirstMoment_eq {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) : MetricCodes.Johnson.clebschFirstMoment✝ w N p q t = ↑t * (↑N - 2 * ↑q - ↑t + 1) * MetricCodes.Johnson.clebschNormSq✝ w N p q t / (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 2)

theorem MetricCodes.Johnson.clebschCoefficient_sq_weighted_harmonic_balance {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) : ∑ r : Fin (t + 1), (↑↑r - 1) * (MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient w p ↑r) = ∑ r : Fin (t + 1), ↑↑r * (MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * Boolean.harmonicCoefficient N q (t - ↑r))

theorem MetricCodes.Johnson.clebschSecondMoment_mul {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) : (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 3) * MetricCodes.Johnson.clebschSecondMoment✝ w N p q t = (↑w - 2 * ↑p + (↑N - 2 * ↑q) * ↑t - ↑t ^ 2 + ↑t + 1) * MetricCodes.Johnson.clebschFirstMoment✝ w N p q t

theorem MetricCodes.Johnson.clebschCoefficient_cross_degree_mul {w N p q t r : ℕ} (hsupport : 2 * p + t ≤ w) (hr : r ≤ t) : MetricCodes.Johnson.clebschCoefficient✝ w N p q (t + 1) r * √(Boolean.harmonicCoefficient N q (t + 1 - r)) = MetricCodes.Johnson.clebschCoefficient✝ w N p q t r * √(Boolean.harmonicCoefficient N q (t + 1))

theorem MetricCodes.Johnson.clebschCoefficient_sq_cross_degree_mul {w N p q t r : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + (t + 1) ≤ N) (hr : r ≤ t) : MetricCodes.Johnson.clebschCoefficient✝ w N p q (t + 1) r ^ 2 * Boolean.harmonicCoefficient N q (t + 1 - r) = MetricCodes.Johnson.clebschCoefficient✝ w N p q t r ^ 2 * Boolean.harmonicCoefficient N q (t + 1)

theorem MetricCodes.Johnson.clebschNormSq_cross_degree_harmonic_balance {w N p q t : ℕ} (hsupport : 2 * p + (t + 1) ≤ w) (hcomplement : 2 * q + (t + 1) ≤ N) : Boolean.harmonicCoefficient N q (t + 1) * MetricCodes.Johnson.clebschNormSq✝ w N p q t = ∑ r : Fin (t + 1 + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q (t + 1) ↑r ^ 2 * Boolean.harmonicCoefficient N q (t + 1 - ↑r)

theorem MetricCodes.Johnson.clebschNormSq_succ_mul {w N p q t : ℕ} (hsupport : 2 * p + (t + 1) ≤ w) (hcomplement : 2 * q + (t + 1) ≤ N) : MetricCodes.Johnson.clebschNormSq✝ w N p q t * ((↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 1) * (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t)) = MetricCodes.Johnson.clebschNormSq✝ w N p q (t + 1) * ((↑w - 2 * ↑p + (↑N - 2 * ↑q) - ↑t + 1) * (↑w - 2 * ↑p - ↑t))

theorem MetricCodes.Johnson.clebschNormSq_div_succ {w N p q t : ℕ} (hsupport : 2 * p + (t + 1) ≤ w) (hcomplement : 2 * q + (t + 1) ≤ N) : MetricCodes.Johnson.clebschNormSq✝ w N p q t / MetricCodes.Johnson.clebschNormSq✝ w N p q (t + 1) = (↑w - 2 * ↑p + (↑N - 2 * ↑q) - ↑t + 1) * (↑w - 2 * ↑p - ↑t) / ((↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 1) * (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t))

theorem MetricCodes.Johnson.clebschCenteredExpectation_eq_johnsonDiagonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (source : Index p q L) : ↑p + MetricCodes.Johnson.clebschFirstMoment✝ w (n - w) p q ↑source / MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q ↑source - ↑w / ↑n * ↑(p + q + ↑source) = johnsonDiagonal n w p q (p + q + ↑source) * (↑w * ↑(n - w) * (↑n - 2 * ↑(p + q + ↑source)) / (↑n * (↑n - 2 * ↑w)))

theorem MetricCodes.Johnson.clebschClosedCenteredExpectation_eq_johnsonDiagonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (source : Index p q L) : ↑p - ↑w / ↑n * ↑(p + q + ↑source) + ↑↑source * (↑(n - w) - 2 * ↑q - ↑↑source + 1) / (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑↑source + 2) = johnsonDiagonal n w p q (p + q + ↑source) * (↑w * ↑(n - w) * (↑n - 2 * ↑(p + q + ↑source)) / (↑n * (↑n - 2 * ↑w)))

theorem MetricCodes.Johnson.johnsonMiddleNormalization_sq_eq_inv_zonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (source : Index p q L) (hsource : 0 < p + q + ↑source) : ((√(MetricCodes.Johnson.johnsonMiddleScale✝ n (p + q + ↑source)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * (↑w * ↑(n - w) * (↑n - 2 * ↑(p + q + ↑source)) / (↑n * (↑n - 2 * ↑w)))) ^ 2 = (johnsonZonalDiagonal n w (p + q + ↑source))⁻¹

theorem MetricCodes.Johnson.johnsonMiddleSignedScalar_eq_sqrt_hattedDiagonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (source : Index p q L) (hsource : 0 < p + q + ↑source) : MetricCodes.Johnson.johnsonDiagonalChannelSign✝ n w p q (p + q + ↑source) * ((√(MetricCodes.Johnson.johnsonMiddleScale✝ n (p + q + ↑source)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * (↑p - ↑w / ↑n * ↑(p + q + ↑source) + ↑↑source * (↑(n - w) - 2 * ↑q - ↑↑source + 1) / (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑↑source + 2))) = √(johnsonHattedDiagonal n w p q (p + q + ↑source))

theorem MetricCodes.Johnson.booleanHarmonicDimension_mul_degreeComplement (n j : ℕ) (hhalf : 2 * j ≤ n) : ↑(booleanHarmonicDimension n j) * (↑n - ↑j + 1) = ↑(n.choose j) * (↑n - 2 * ↑j + 1)

theorem MetricCodes.Johnson.booleanHarmonicDimension_succ_div {n j : ℕ} (hhalf : 2 * (j + 1) ≤ n) : ↑(booleanHarmonicDimension n (j + 1)) / ↑(booleanHarmonicDimension n j) = (↑n - 2 * ↑j - 1) * (↑n - ↑j + 1) / ((↑j + 1) * (↑n - 2 * ↑j + 1))

theorem MetricCodes.Johnson.booleanHarmonicDimension_succ_div_eq_upperScale {n j : ℕ} (hhalf : 2 * (j + 1) ≤ n) : ↑(booleanHarmonicDimension n (j + 1)) / ↑(booleanHarmonicDimension n j) = MetricCodes.Johnson.johnsonUpperScale✝ n j / (↑j + 1)

theorem MetricCodes.Johnson.clebschCenteredAxis_sum (w N p q t : ℕ) (c : ℝ) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * (↑(p + ↑r) - c * ↑(p + q + t)) = (↑p - c * ↑(p + q + t)) * MetricCodes.Johnson.clebschNormSq✝ w N p q t + MetricCodes.Johnson.clebschFirstMoment✝ w N p q t

theorem MetricCodes.Johnson.clebschCenteredAxis_sum_eq {w N p q t : ℕ} (hsupport : 2 * p + t ≤ w) (hcomplement : 2 * q + t ≤ N) (c : ℝ) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r ^ 2 * (↑(p + ↑r) - c * ↑(p + q + t)) = MetricCodes.Johnson.clebschNormSq✝ w N p q t * (↑p - c * ↑(p + q + t) + ↑t * (↑N - 2 * ↑q - ↑t + 1) / (↑w - 2 * ↑p + (↑N - 2 * ↑q) - 2 * ↑t + 2))

theorem MetricCodes.Johnson.clebschSignedAdjacentCross_sum {w N p q t : ℕ} (hsupport : 2 * p + (t + 1) ≤ w) (_hcomplement : 2 * q + (t + 1) ≤ N) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.clebschCoefficient✝ w N p q (t + 1) (↑r + 1) = -√(Boolean.harmonicCoefficient N q (t + 1)) * MetricCodes.Johnson.clebschNormSq✝ w N p q t

theorem MetricCodes.Johnson.johnsonAxisRaise_coupledHarmonic_dot_closed {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + (t + 1)) f) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisRaise✝ x (coupledHarmonic x hp hq a t)) = -√(↑n / (↑w * ↑(n - w))) * √(Boolean.harmonicCoefficient (n - w) q (t + 1)) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) / √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1))) * Boolean.dot f (coupledHarmonic x hp hq a (t + 1))

theorem MetricCodes.Johnson.johnsonLowerChannel_coupled_axis_inner_closed {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + (t + 1)) f) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonLowerChannel✝ (p + q + (t + 1)) f) (johnsonAxisTensor x (coupledHarmonic x hp hq a t)) = -(√↑(p + q + (t + 1)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * √(Boolean.harmonicCoefficient (n - w) q (t + 1)) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) / √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1))) * Boolean.dot f (coupledHarmonic x hp hq a (t + 1))

theorem MetricCodes.Johnson.clebschSignedAdjacentCross_sum_comm {w N p q t : ℕ} (hsupport : 2 * p + (t + 1) ≤ w) (hcomplement : 2 * q + (t + 1) ≤ N) : ∑ r : Fin (t + 1), MetricCodes.Johnson.clebschCoefficient✝ w N p q (t + 1) (↑r + 1) * √(Boolean.harmonicCoefficient w p (↑r + 1)) * MetricCodes.Johnson.clebschCoefficient✝ w N p q t ↑r = -√(Boolean.harmonicCoefficient N q (t + 1)) * MetricCodes.Johnson.clebschNormSq✝ w N p q t

theorem MetricCodes.Johnson.johnsonAxisLower_coupledHarmonic_dot_closed {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisLower✝ x (coupledHarmonic x hp hq a (t + 1))) = -√(↑n / (↑w * ↑(n - w))) * √(Boolean.harmonicCoefficient (n - w) q (t + 1)) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) / √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1))) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.johnsonUpperChannel_coupled_axis_inner_closed {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + (t + 1) ≤ w) (htcomplement : 2 * q + (t + 1) ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonUpperChannel✝ (p + q + t) f) (johnsonAxisTensor x (coupledHarmonic x hp hq a (t + 1))) = -(√(MetricCodes.Johnson.johnsonUpperScale✝ n (p + q + t)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * √(Boolean.harmonicCoefficient (n - w) q (t + 1)) * (√(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) / √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1))) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.coupledHarmonic_dot_of_split_proportional {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hpair : ∀ (r : Fin (t + 1)), Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r)) = MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)) : Boolean.dot f (coupledHarmonic x hp hq a t) = √(MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t) * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)

theorem MetricCodes.Johnson.johnsonAxisMembership_coupledHarmonic_dot_of_split_proportional {n w p q t : ℕ} (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hpair : ∀ (r : Fin (t + 1)), Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r)) = MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)) : Boolean.dot f (MetricCodes.Johnson.johnsonAxisMembership✝ x (coupledHarmonic x hp hq a t)) = √(↑n / (↑w * ↑(n - w))) * (↑p - ↑w / ↑n * ↑(p + q + t) + ↑t * (↑(n - w) - 2 * ↑q - ↑t + 1) / (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑t + 2)) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.johnsonMiddleChannel_coupled_axis_inner_of_split_proportional {n w p q t : ℕ} (hn : 0 < n) (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hpair : ∀ (r : Fin (t + 1)), Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a (↑r) (t - ↑r)) = MetricCodes.Johnson.clebschCoefficient✝ w (n - w) p q t ↑r * Boolean.dot f (MetricCodes.Johnson.splitTensor✝ x hp hq a 0 t)) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonMiddleChannel✝ (p + q + t) f) (johnsonAxisTensor x (coupledHarmonic x hp hq a t)) = (√(MetricCodes.Johnson.johnsonMiddleScale✝ n (p + q + t)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * (↑p - ↑w / ↑n * ↑(p + q + t) + ↑t * (↑(n - w) - 2 * ↑q - ↑t + 1) / (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑t + 2)) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.johnsonMiddleChannel_coupled_axis_inner_closed {n w p q t : ℕ} (hn : 0 < n) (x : JohnsonSphere n w) (hp : 2 * p ≤ w) (hq : 2 * q ≤ n - w) (htsupport : 2 * p + t ≤ w) (htcomplement : 2 * q + t ≤ n - w) (a : HarmonicFibreIndex n w p q) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + t) f) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonMiddleChannel✝ (p + q + t) f) (johnsonAxisTensor x (coupledHarmonic x hp hq a t)) = (√(MetricCodes.Johnson.johnsonMiddleScale✝ n (p + q + t)))⁻¹ * √(↑n / (↑w * ↑(n - w))) * (↑p - ↑w / ↑n * ↑(p + q + t) + ↑t * (↑(n - w) - 2 * ↑q - ↑t + 1) / (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑t + 2)) * Boolean.dot f (coupledHarmonic x hp hq a t)

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_diagonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (source : Index p q L) : johnsonSourceChannelCoefficient n w p q L source source = johnsonHattedDiagonal n w p q (p + q + ↑source)

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_reverse_mul_upperScale {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : johnsonSourceChannelCoefficient n w p q L target source * MetricCodes.Johnson.johnsonUpperScale✝ n (p + q + ↑target) = johnsonSourceChannelCoefficient n w p q L source target * (↑(p + q + ↑target) + 1)

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_reverse_eq_upperScale {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : johnsonSourceChannelCoefficient n w p q L target source = johnsonSourceChannelCoefficient n w p q L source target * (↑(p + q + ↑target) + 1) / MetricCodes.Johnson.johnsonUpperScale✝ n (p + q + ↑target)

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_reverse_sqrt_eq_upperScale {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : √(johnsonSourceChannelCoefficient n w p q L target source) = √(johnsonSourceChannelCoefficient n w p q L source target) * √(↑(p + q + ↑target) + 1) / √(MetricCodes.Johnson.johnsonUpperScale✝ n (p + q + ↑target))

theorem MetricCodes.Johnson.johnsonMiddleChannel_signed_axis_inner {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : JohnsonSphere n w) (source : Index p q L) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (a : HarmonicFibreIndex n w p q) (hsource : 0 < p + q + ↑source) : Boolean.coordinateDot (MetricCodes.Johnson.johnsonDiagonalChannelSign✝ n w p q (p + q + ↑source) • MetricCodes.Johnson.johnsonMiddleChannel✝ (p + q + ↑source) f) (johnsonAxisTensor x (coupledHarmonic x ⋯ ⋯ a ↑source)) = √(johnsonSourceChannelCoefficient n w p q L source source) * Boolean.dot f (coupledHarmonic x ⋯ ⋯ a ↑source)

theorem MetricCodes.Johnson.johnsonAdjacentChannel_axis_inner_of_not_active {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n) (a : HarmonicFibreIndex n w p q) (hinactive : ¬johnsonChannelActive p q L target source) : Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target source f) (johnsonAxisTensor x (coupledHarmonic x ⋯ ⋯ a ↑target)) = √(johnsonSourceChannelCoefficient n w p q L source target) * Boolean.dot f (coupledHarmonic x ⋯ ⋯ a ↑source)

theorem MetricCodes.Johnson.johnsonAdjacentChannel_axis_inner_diagonal {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : JohnsonSphere n w) (source : Index p q L) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (a : HarmonicFibreIndex n w p q) : Boolean.coordinateDot (johnsonAdjacentChannel n w p q L source source f) (johnsonAxisTensor x (coupledHarmonic x ⋯ ⋯ a ↑source)) = √(johnsonSourceChannelCoefficient n w p q L source source) * Boolean.dot f (coupledHarmonic x ⋯ ⋯ a ↑source)

theorem MetricCodes.Johnson.johnsonOffDiagonal_fourthPower_grouped_algebra {N W C G j A B E F : ℝ} (hN : N ≠ 0) (hW : W ≠ 0) (hC : C ≠ 0) (hWj : W - j ≠ 0) (hCj : C - j ≠ 0) (hG : G ≠ 0) (hGminus : G - 1 ≠ 0) (hGplus : G + 1 ≠ 0) (hjone : j + 1 ≠ 0) (hlast : N - j + 1 ≠ 0) : (N * A * B * E * F) ^ 2 / (W * C * G * (G + 1)) ^ 2 / (j + 1) ^ 2 = (N ^ 2 * ((W - j) * (C - j) * A * B * E * F) / ((W * C) ^ 2 * G ^ 2 * ((G - 1) * (G + 1)))) ^ 2 / (N ^ 2 * ((W - j) ^ 2 * (C - j) ^ 2 * (j + 1) * (N - j + 1)) / ((W * C) ^ 2 * G ^ 2 * ((G - 1) * (G + 1)))) * ((G - 1) * (N - j + 1) / ((j + 1) * (G + 1)))

theorem MetricCodes.Johnson.johnsonAdjacentRawSquare_compact_algebra {N W C P Q T : ℝ} (hNC : N = W + C) (hW : W ≠ 0) (hC : C ≠ 0) (hgap : N - 2 * (P + Q + T) ≠ 0) (hgapplus : N - 2 * (P + Q + T) + 1 ≠ 0) : N / (W * C) * ((T + 1) * (C - 2 * Q - T)) * ((W - 2 * P + (C - 2 * Q) - T + 1) * (W - 2 * P - T) / ((W - 2 * P + (C - 2 * Q) - 2 * T + 1) * (W - 2 * P + (C - 2 * Q) - 2 * T))) = N * (W - (P + Q + T) - P + Q) * (C - (P + Q + T) + P - Q) * (P + Q + T - P - Q + 1) * (N - P - Q - (P + Q + T) + 1) / (W * C * (N - 2 * (P + Q + T)) * (N - 2 * (P + Q + T) + 1))

theorem MetricCodes.Johnson.johnsonNu_radicand_factor {n w p q j : ℕ} (hwn : w ≤ n) : (johnsonJ n j ^ 2 - johnsonM n w ^ 2) * (johnsonJ n j ^ 2 - johnsonDelta n w p q ^ 2) * ((johnsonSigma n w p q + 1) ^ 2 - johnsonJ n j ^ 2) = (↑w - ↑j) * (↑(n - w) - ↑j) * (↑w - ↑j - ↑p + ↑q) * (↑(n - w) - ↑j + ↑p - ↑q) * (↑j - ↑p - ↑q + 1) * (↑n - ↑p - ↑q - ↑j + 1)

theorem MetricCodes.Johnson.johnsonNu_denominator_factor (n j : ℕ) : (2 * johnsonJ n j - 1) * (2 * johnsonJ n j + 1) = (↑n - 2 * ↑j - 1) * (↑n - 2 * ↑j + 1)

theorem MetricCodes.Johnson.johnsonNu_radicand_pos {n w p q L j : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (hfirst : p + q ≤ j) (hlast : j < johnsonLastDegree n w p q) : 0 < (johnsonJ n j ^ 2 - johnsonM n w ^ 2) * (johnsonJ n j ^ 2 - johnsonDelta n w p q ^ 2) * ((johnsonSigma n w p q + 1) ^ 2 - johnsonJ n j ^ 2)

theorem MetricCodes.Johnson.johnsonNu_denominator_pos {n w p q L j : ℕ} : AdmissibleDegrees n w p q L → ∀ (hstrict : 2 * w < n) (hlast : j < johnsonLastDegree n w p q), 0 < (2 * johnsonJ n j - 1) * (2 * johnsonJ n j + 1)

theorem MetricCodes.Johnson.johnsonEdge_sq_factored {n w p q L j : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (hfirst : p + q ≤ j) (hlast : j < johnsonLastDegree n w p q) : johnsonEdge n w p q j ^ 2 = ↑n ^ 2 * ((↑w - ↑j) * (↑(n - w) - ↑j) * (↑w - ↑j - ↑p + ↑q) * (↑(n - w) - ↑j + ↑p - ↑q) * (↑j - ↑p - ↑q + 1) * (↑n - ↑p - ↑q - ↑j + 1)) / ((↑w * ↑(n - w)) ^ 2 * (↑n - 2 * ↑j) ^ 2 * ((↑n - 2 * ↑j - 1) * (↑n - 2 * ↑j + 1)))

theorem MetricCodes.Johnson.johnsonZonalEdge_sq_factored {n w p q L j : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (hjw : j < w) : johnsonZonalEdge n w j ^ 2 = ↑n ^ 2 * ((↑w - ↑j) ^ 2 * (↑(n - w) - ↑j) ^ 2 * (↑j + 1) * (↑n - ↑j + 1)) / ((↑w * ↑(n - w)) ^ 2 * (↑n - 2 * ↑j) ^ 2 * ((↑n - 2 * ↑j - 1) * (↑n - 2 * ↑j + 1)))

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_sq {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (source target : Index p q L) : johnsonSourceChannelCoefficient n w p q L source target ^ 2 = matrix n w p q L source target ^ 2 * (↑(booleanHarmonicDimension n (p + q + ↑source)) / ↑(booleanHarmonicDimension n (p + q + ↑target)))

theorem MetricCodes.Johnson.johnsonAdjacentRawScalar_sq {n w p q t : ℕ} (hw : 0 < w) (hwn : w < n) : 2 * p + (t + 1) ≤ w → ∀ (hcomplement : 2 * q + (t + 1) ≤ n - w), MetricCodes.Johnson.johnsonAdjacentRawScalar✝ n w p q t ^ 2 = ↑n / (↑w * ↑(n - w)) * Boolean.harmonicCoefficient (n - w) q (t + 1) * (MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q t / MetricCodes.Johnson.clebschNormSq✝ w (n - w) p q (t + 1))

theorem MetricCodes.Johnson.johnsonAdjacentRawScalar_sq_factored {n w p q t : ℕ} (hw : 0 < w) (hwn : w < n) (hsupport : 2 * p + (t + 1) ≤ w) (hcomplement : 2 * q + (t + 1) ≤ n - w) : MetricCodes.Johnson.johnsonAdjacentRawScalar✝ n w p q t ^ 2 = ↑n / (↑w * ↑(n - w)) * ((↑t + 1) * (↑(n - w) - 2 * ↑q - ↑t)) * ((↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - ↑t + 1) * (↑w - 2 * ↑p - ↑t) / ((↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑t + 1) * (↑w - 2 * ↑p + (↑(n - w) - 2 * ↑q) - 2 * ↑t)))

theorem MetricCodes.Johnson.johnsonAdjacentRawScalar_pos {n w p q t : ℕ} (hw : 0 < w) (hwn : w < n) : 2 * p + (t + 1) ≤ w → ∀ (hcomplement : 2 * q + (t + 1) ≤ n - w), 0 < MetricCodes.Johnson.johnsonAdjacentRawScalar✝ n w p q t

theorem MetricCodes.Johnson.johnsonLowerOffDiagonalScalar_sq {n w p q t : ℕ} : 0 < p + q + (t + 1) → MetricCodes.Johnson.johnsonLowerOffDiagonalScalar✝ n w p q t ^ 2 = MetricCodes.Johnson.johnsonAdjacentRawScalar✝ n w p q t ^ 2 / ↑(p + q + (t + 1))

theorem MetricCodes.Johnson.johnsonSourceChannelCoefficient_lower_sq {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : johnsonSourceChannelCoefficient n w p q L source target ^ 2 = johnsonHattedEdge n w p q (p + q + ↑target) ^ 2 * (↑(booleanHarmonicDimension n (p + q + ↑source)) / ↑(booleanHarmonicDimension n (p + q + ↑target)))

theorem MetricCodes.Johnson.johnsonAdjacentRawScalar_sq_degree_factored {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : MetricCodes.Johnson.johnsonAdjacentRawScalar✝ n w p q ↑target ^ 2 = ↑n * (↑w - ↑(p + q + ↑target) - ↑p + ↑q) * (↑(n - w) - ↑(p + q + ↑target) + ↑p - ↑q) * (↑(p + q + ↑target) - ↑p - ↑q + 1) * (↑n - ↑p - ↑q - ↑(p + q + ↑target) + 1) / (↑w * ↑(n - w) * (↑n - 2 * ↑(p + q + ↑target)) * (↑n - 2 * ↑(p + q + ↑target) + 1))

theorem MetricCodes.Johnson.johnsonLowerOffDiagonalScalar_fourthPower {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : MetricCodes.Johnson.johnsonLowerOffDiagonalScalar✝ n w p q ↑target ^ 4 = johnsonSourceChannelCoefficient n w p q L source target ^ 2

theorem MetricCodes.Johnson.johnsonLowerOffDiagonalScalar_eq_sqrt_source {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : MetricCodes.Johnson.johnsonLowerOffDiagonalScalar✝ n w p q ↑target = √(johnsonSourceChannelCoefficient n w p q L source target)

theorem MetricCodes.Johnson.johnsonUpperOffDiagonalScalar_eq_sqrt_source {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (target source : Index p q L) (hadj : ↑target + 1 = ↑source) : MetricCodes.Johnson.johnsonUpperOffDiagonalScalar✝ n w p q ↑target = √(johnsonSourceChannelCoefficient n w p q L target source)

theorem MetricCodes.Johnson.johnsonCoordinateDot_smul_left {n : ℕ} (c : ℝ) (f g : Boolean.CoordinateFunction n) : Boolean.coordinateDot (c • f) g = c * Boolean.coordinateDot f g

theorem MetricCodes.Johnson.johnsonAdjacentChannel_axis_inner {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n) (hf : Boolean.IsHarmonic (p + q + ↑source) f) (a : HarmonicFibreIndex n w p q) : Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target source f) (johnsonAxisTensor x (coupledHarmonic x ⋯ ⋯ a ↑target)) = √(johnsonSourceChannelCoefficient n w p q L source target) * Boolean.dot f (coupledHarmonic x ⋯ ⋯ a ↑source)