Strict rate improvements

The MRRW comparison and the first spherical hierarchy and numerical bounds.

theorem MetricCodes.MRRW.hasDerivAt_mul_continuous_zero (g : ℝ → ℝ) (hg : ContinuousAt g 0) (hgzero : g 0 = 0) : HasDerivAt (fun (r : ℝ) => r * g r) 0 0

theorem MetricCodes.MRRW.inverseVarianceFactor_continuous : Continuous MetricCodes.MRRW.inverseVarianceFactor✝

theorem MetricCodes.MRRW.inverseDegree_eq_sq_mul_factor {r : ℝ} (hr : r ^ 2 ≤ 1) : MetricCodes.MRRW.inverseDegree✝ r = r * (r * MetricCodes.MRRW.inverseVarianceFactor✝ r)

theorem MetricCodes.MRRW.inverseEntropyFactor_continuous : Continuous MetricCodes.MRRW.inverseEntropyFactor✝

@[simp]

theorem MetricCodes.MRRW.inverseEntropyFactor_zero : MetricCodes.MRRW.inverseEntropyFactor✝ 0 = 0

theorem MetricCodes.MRRW.negMulLog_inverseDegree_eventually : (fun (r : ℝ) => (MetricCodes.MRRW.inverseDegree✝ r).negMulLog) =ᶠ[nhds 0] fun (r : ℝ) => r * MetricCodes.MRRW.inverseEntropyFactor✝ r

theorem MetricCodes.MRRW.hasDerivAt_negMulLog_inverseDegree_zero : HasDerivAt (fun (r : ℝ) => (MetricCodes.MRRW.inverseDegree✝ r).negMulLog) 0 0

theorem MetricCodes.MRRW.hasDerivAt_inverseDegree_zero : HasDerivAt MetricCodes.MRRW.inverseDegree✝ 0 0

theorem MetricCodes.MRRW.hasDerivAt_mrrwG_sq_zero : HasDerivAt (fun (r : ℝ) => Johnson.mrrwG (r ^ 2)) 0 0

theorem MetricCodes.MRRW.lowerEndpointRoot_pos {δ : ℝ} (hhalf : δ < 1 / 2) : 0 < MetricCodes.MRRW.lowerEndpointRoot✝ δ

theorem MetricCodes.MRRW.lowerEndpointRoot_lt_one {δ : ℝ} (hδ : 0 < δ) : MetricCodes.MRRW.lowerEndpointRoot✝ δ < 1

theorem MetricCodes.MRRW.lowerEndpointWeight_pos {δ : ℝ} (hδ : 0 < δ) : 0 < MetricCodes.MRRW.lowerEndpointWeight✝ δ

theorem MetricCodes.MRRW.lowerEndpointWeight_lt_half {δ : ℝ} (hhalf : δ < 1 / 2) : MetricCodes.MRRW.lowerEndpointWeight✝ δ < 1 / 2

theorem MetricCodes.MRRW.lowerEndpointDerivative_pos {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : 0 < MetricCodes.MRRW.lowerEndpointDerivative✝ δ

theorem MetricCodes.MRRW.hasDerivAt_mrrwG_boundary_quadratic_zero {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : HasDerivAt (fun (r : ℝ) => Johnson.mrrwG (r ^ 2 + 2 * δ * r + 2 * δ)) (MetricCodes.MRRW.lowerEndpointDerivative✝ δ) 0

theorem MetricCodes.MRRW.hasDerivAt_mrrwObjective_zero {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : HasDerivAt (Johnson.mrrwObjective δ) (-MetricCodes.MRRW.lowerEndpointDerivative✝ δ) 0

theorem MetricCodes.MRRW.exists_mrrwObjective_lt_zero {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : ∃ (r : ℝ), 0 < r ∧ r < 1 - 2 * δ ∧ Johnson.mrrwObjective δ r < Johnson.mrrwObjective δ 0

theorem MetricCodes.MRRW.mrrw_minimizer_pos {δ r : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) (hr : 0 ≤ r) (hupper : r ≤ 1 - 2 * δ) (hmin : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 - 2 * δ → Johnson.mrrwObjective δ r ≤ Johnson.mrrwObjective δ s) : 0 < r

theorem MetricCodes.MRRW.exists_positive_mrrw_minimizer {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : ∃ (r : ℝ), 0 < r ∧ r ≤ 1 - 2 * δ ∧ (∀ (s : ℝ), 0 ≤ s → s ≤ 1 - 2 * δ → Johnson.mrrwObjective δ r ≤ Johnson.mrrwObjective δ s) ∧ Johnson.mrrwRate δ = Johnson.mrrwObjective δ r

theorem MetricCodes.MRRW.inverse_zero_fibre_boundary {δ r : ℝ} (hδ : 0 < δ) : δ < 1 / 2 → ∀ (hr : 0 < r) (hupper : r < 1 - 2 * δ), ∃ (a : ℝ) (u : ℝ), 0 < u ∧ u < a ∧ a < 1 / 2 ∧ δ / 2 < a ∧ Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a ∧ Johnson.mrrwObjective δ r = Johnson.shellRate a 0 0 u

theorem MetricCodes.MRRW.exists_zero_fibre_boundary_of_interior_minimizer {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) (hstrict : Johnson.mrrwRate δ < Hamming.classicalRate δ) : ∃ (a : ℝ) (u : ℝ), 0 < u ∧ u < a ∧ a < 1 / 2 ∧ δ / 2 < a ∧ Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a ∧ Johnson.mrrwRate δ = Johnson.shellRate a 0 0 u

@[simp]

theorem MetricCodes.MRRW.interiorWeight_zero (a u : ℝ) : MetricCodes.MRRW.interiorWeight✝ a u 0 = a

@[simp]

theorem MetricCodes.MRRW.interiorSupport_zero (a u : ℝ) : MetricCodes.MRRW.interiorSupport✝ a u 0 = 0

@[simp]

theorem MetricCodes.MRRW.interiorComplement_zero (a u : ℝ) : MetricCodes.MRRW.interiorComplement✝ a u 0 = 0

theorem MetricCodes.MRRW.interiorSupport_add_complement (a u e : ℝ) : MetricCodes.MRRW.interiorSupport✝ a u e + MetricCodes.MRRW.interiorComplement✝ a u e = e

theorem MetricCodes.MRRW.rankPenalty_interior {a u e : ℝ} (hweight : 0 < MetricCodes.MRRW.interiorWeight✝ a u e) (hweight' : MetricCodes.MRRW.interiorWeight✝ a u e < 1) : Johnson.rankPenalty (MetricCodes.MRRW.interiorWeight✝ a u e) (MetricCodes.MRRW.interiorSupport✝ a u e) (MetricCodes.MRRW.interiorComplement✝ a u e) = binaryEntropy e

theorem MetricCodes.MRRW.tendsto_interiorWeight_zero (a u : ℝ) : Filter.Tendsto (MetricCodes.MRRW.interiorWeight✝ a u) (nhdsWithin 0 (Set.Ioi 0)) (nhds a)

theorem MetricCodes.MRRW.eventually_binaryEntropy_inward_improvement {a : ℝ} (ha : 0 < a) (ha' : a < 1) (C : ℝ) : ∀ᶠ (e : ℝ) in nhdsWithin 0 (Set.Ioi 0), binaryEntropy a - binaryEntropy (a - C * e) < binaryEntropy e

theorem MetricCodes.MRRW.eventually_shellRate_interior_improvement {a u : ℝ} (ha : 0 < a) (ha' : a < 1 / 2) : ∀ᶠ (e : ℝ) in nhdsWithin 0 (Set.Ioi 0), Johnson.shellRate (MetricCodes.MRRW.interiorWeight✝ a u e) (MetricCodes.MRRW.interiorSupport✝ a u e) (MetricCodes.MRRW.interiorComplement✝ a u e) u < Johnson.shellRate a 0 0 u

theorem MetricCodes.MRRW.interiorSpectralMargin_zero {δ a u : ℝ} (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : MetricCodes.MRRW.interiorSpectralMargin✝ δ a u 0 = 0

theorem MetricCodes.MRRW.interior_boundary_delta_relation {δ a u : ℝ} (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : δ * (1 + 2 * √(u * (1 - u))) = 2 * (a * (1 - a) - u * (1 - u))

theorem MetricCodes.MRRW.interior_boundary_weight_gt_distance {δ a u : ℝ} (hδ : 0 < δ) (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : δ / 2 < a

theorem MetricCodes.MRRW.spectralLimit_interior_eq (a u e : ℝ) : Johnson.spectralLimit (MetricCodes.MRRW.interiorWeight✝ a u e) (MetricCodes.MRRW.interiorSupport✝ a u e) (MetricCodes.MRRW.interiorComplement✝ a u e) u = have z := 1 - 2 * u; have m := 1 - 2 * MetricCodes.MRRW.interiorWeight✝ a u e; have t := 1 - 2 * e; (m * (t ^ 2 - z ^ 2)) ^ 2 / (z ^ 2 * (1 - m ^ 2) * (1 - z ^ 2)) + (z ^ 2 - (m * t) ^ 2) * (t ^ 2 - z ^ 2) / (z ^ 2 * (1 - m ^ 2) * √(1 - z ^ 2))

theorem MetricCodes.MRRW.eventually_interior_parameters {δ a u : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) (hδa : δ / 2 < a) (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) : ∀ᶠ (e : ℝ) in nhdsWithin 0 (Set.Ioi 0), Johnson.AsymptoticParameters δ (MetricCodes.MRRW.interiorWeight✝ a u e) (MetricCodes.MRRW.interiorSupport✝ a u e) (MetricCodes.MRRW.interiorComplement✝ a u e) u

theorem MetricCodes.MRRW.hasDerivAt_interiorSpectralMargin {δ a u : ℝ} (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : HasDerivAt (MetricCodes.MRRW.interiorSpectralMargin✝ δ a u) ((1 - 2 * (a * (1 - a))) * (1 - 2 * √(u * (1 - u))) / (a * (1 - a) * √(u * (1 - u)) * (1 + 2 * √(u * (1 - u))))) 0

theorem MetricCodes.MRRW.interiorSpectralMargin_derivative_pos {a u : ℝ} (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) : 0 < (1 - 2 * (a * (1 - a))) * (1 - 2 * √(u * (1 - u))) / (a * (1 - a) * √(u * (1 - u)) * (1 + 2 * √(u * (1 - u))))

theorem MetricCodes.MRRW.eventually_interiorSpectralMargin_pos {δ a u : ℝ} (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : ∀ᶠ (e : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < MetricCodes.MRRW.interiorSpectralMargin✝ δ a u e

theorem MetricCodes.MRRW.eventually_interior_feasible {δ a u : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : ∀ᶠ (e : ℝ) in nhdsWithin 0 (Set.Ioi 0), Johnson.Feasible δ (MetricCodes.MRRW.interiorWeight✝ a u e) (MetricCodes.MRRW.interiorSupport✝ a u e) (MetricCodes.MRRW.interiorComplement✝ a u e) u

theorem MetricCodes.MRRW.interior_shell_improvement {δ a u : ℝ} (hδ : 0 < δ) (hδ' : δ < 1 / 2) (hu : 0 < u) (hua : u < a) (ha : a < 1 / 2) (hboundary : Johnson.spectralLimit a 0 0 u = Johnson.asymptoticThreshold δ a) : ∃ (A : ℝ) (b : ℝ) (g : ℝ), 0 < b ∧ 0 < g ∧ Johnson.Feasible δ A b g u ∧ Johnson.shellRate A b g u < Johnson.shellRate a 0 0 u

theorem MetricCodes.MRRW.variationalRate_lt_mrrw_of_interior {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) (hstrict : Johnson.mrrwRate δ < Hamming.classicalRate δ) : Johnson.variationalRate δ < Johnson.mrrwRate δ

theorem MetricCodes.MRRW.strict_mrrw2 {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : Johnson.combinedVariationalRate δ < Johnson.mrrwRate δ

theorem MetricCodes.Johnson.johnsonWindowBasis_isHarmonic {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (Q : ShellWindowIndex n p q L) : Boolean.IsHarmonic (p + q + ↑Q.fst) (MetricCodes.Johnson.johnsonWindowBasis✝ h Q)

theorem MetricCodes.Johnson.johnsonHarmonicCoordinates_pairing {n j : ℕ} (hj : 2 * j ≤ n) (f g : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (hg : Boolean.IsHarmonic j g) : ∑ a : Fin (booleanHarmonicDimension n j), MetricCodes.Johnson.johnsonHarmonicCoordinates✝ hj f hf a * MetricCodes.Johnson.johnsonHarmonicCoordinates✝ hj g hg a = Boolean.dot f g

theorem MetricCodes.Johnson.johnsonWindowBasis_dot {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (source : Index p q L) (a b : Fin (booleanHarmonicDimension n (p + q + ↑source))) : Boolean.dot (MetricCodes.Johnson.johnsonWindowBasis✝ h ⟨source, a⟩) (MetricCodes.Johnson.johnsonWindowBasis✝ h ⟨source, b⟩) = if a = b then 1 else 0

theorem MetricCodes.Johnson.globalHarmonicVector_harmonicBasisFunction {n j : ℕ} (hj : 2 * j ≤ n) (a : Fin (booleanHarmonicDimension n j)) : globalHarmonicVector (Boolean.harmonicBasisFunction n j hj a) ⋯ = (Boolean.harmonicOrthonormalBasis n j hj) a

theorem MetricCodes.Johnson.johnsonHarmonicCoordinates_eq_basis_dot {n j : ℕ} (hj : 2 * j ≤ n) (f : Boolean.Function n) (hf : Boolean.IsHarmonic j f) (a : Fin (booleanHarmonicDimension n j)) : MetricCodes.Johnson.johnsonHarmonicCoordinates✝ hj f hf a = Boolean.dot (Boolean.harmonicBasisFunction n j hj a) f

theorem MetricCodes.Johnson.johnsonWindowBasis_dot_coupled {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (x : JohnsonSphere n w) (source : Index p q L) (a : HarmonicFibreIndex n w p q) (b : Fin (booleanHarmonicDimension n (p + q + ↑source))) : Boolean.dot (MetricCodes.Johnson.johnsonWindowBasis✝ h ⟨source, b⟩) (coupledHarmonic x ⋯ ⋯ a ↑source) = coupledDegreeCoordinates h x source a b

theorem MetricCodes.Johnson.johnsonWindowChannelMatrix_pairing {n w p q L : ℕ} (h : AdmissibleDegrees n w p q L) (hstrict : 2 * w < n) (v : Space p q L) (lam : ℝ) (Q R : ShellWindowIndex n p q L) : ∑ T : Fin n × ShellWindowIndex n p q L, MetricCodes.Johnson.johnsonWindowChannelMatrix✝ h hstrict v lam T Q * MetricCodes.Johnson.johnsonWindowChannelMatrix✝ h hstrict v lam T R = ∑ target : Index p q L, johnsonAdjacentBlockCoefficient n w p q L v lam target Q.fst * johnsonAdjacentBlockCoefficient n w p q L v lam target R.fst * Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target Q.fst (MetricCodes.Johnson.johnsonWindowBasis✝ h Q)) (johnsonAdjacentChannel n w p q L target R.fst (MetricCodes.Johnson.johnsonWindowBasis✝ h R))

theorem MetricCodes.Johnson.johnsonWindowChannelMatrix_transpose_mul {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) : (MetricCodes.Johnson.johnsonWindowChannelMatrix✝ h hstrict v lam).transpose * MetricCodes.Johnson.johnsonWindowChannelMatrix✝ h hstrict v lam = 1

theorem MetricCodes.Johnson.johnsonChannelMatrix_transpose_mul {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) : (MetricCodes.Johnson.johnsonChannelMatrix✝ h hstrict v lam).transpose * MetricCodes.Johnson.johnsonChannelMatrix✝ h hstrict v lam = 1

theorem MetricCodes.Johnson.johnsonAdjacentChannel_coordinate_axisDot {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) : ∑ k : Fin n, ∑ b : Fin (booleanHarmonicDimension n (p + q + ↑target)), (geometricAxis x).ofLp k * MetricCodes.Johnson.johnsonHarmonicCoordinates✝ ⋯ (johnsonAdjacentChannel n w p q L target source f k) ⋯ b * coupledDegreeCoordinates h x target a b = Boolean.coordinateDot (johnsonAdjacentChannel n w p q L target source f) (johnsonAxisTensor x (coupledHarmonic x ⋯ ⋯ a ↑target))

theorem MetricCodes.Johnson.johnsonWindowChannelMatrix_transpose_axis_fibre {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) (haxis : ∀ (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n), 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)) (x : JohnsonSphere n w) : (MetricCodes.Johnson.johnsonWindowChannelMatrix✝ h hstrict v lam).transpose * Boolean.matrixAxisLift (fun (k : Fin n) => (geometricAxis x).ofLp k) (johnsonWindowFibreMatrix h v x) = √lam • johnsonWindowFibreMatrix h v x

theorem MetricCodes.Johnson.johnsonChannelMatrix_transpose_axis_fibre {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) (haxis : ∀ (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n), 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)) (x : JohnsonSphere n w) : (MetricCodes.Johnson.johnsonChannelMatrix✝ h hstrict v lam).transpose * Boolean.matrixAxisLift (fun (k : Fin n) => (geometricAxis x).ofLp k) (johnsonFibreMatrix h v x) = √lam • johnsonFibreMatrix h v x

theorem MetricCodes.Johnson.johnsonChannelMatrix_transpose_axis_projection {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) (haxis : ∀ (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n), 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)) (x : JohnsonSphere n w) : (MetricCodes.Johnson.johnsonChannelMatrix✝ h hstrict v lam).transpose * Boolean.matrixAxisLift (fun (k : Fin n) => (geometricAxis x).ofLp k) ((johnsonProjectionFamily h v hv).projection x) = √lam • (johnsonProjectionFamily h v hv).projection x

theorem MetricCodes.Johnson.johnsonProjectionGramFeature_inner {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) (haxis : ∀ (x : JohnsonSphere n w) (target source : Index p q L) (f : Boolean.Function n), 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)) (x y : JohnsonSphere n w) : inner ℝ (MetricCodes.Johnson.johnsonProjectionGramFeature✝ h hstrict v hv lam x) (MetricCodes.Johnson.johnsonProjectionGramFeature✝ h hstrict v hv lam y) = (correlation x y - lam) * (johnsonProjectionFamily h v hv).overlap x y

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_terminalIndex_ratio {u : ℝ} (hu : 0 < u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n) / ↑n) Filter.atTop (nhds u)

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_add_degree_add_fixed_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)) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(f n + g n + r) / ↑n) Filter.atTop (nhds (a + b))

theorem MetricCodes.Johnson.SpectralAsymptotics.eventually_terminal_block_fit {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, Asymptotics.supportDegree b n + Asymptotics.complementDegree g n + r < Asymptotics.terminalDegree u n

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

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonJ1_ratio {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : Filter.Tendsto (fun (n : ℕ) => johnsonJ1 (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) / ↑n) Filter.atTop (nhds (a / 2 - b))

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonJ2_ratio {a g : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) (hg : 0 ≤ g) : Filter.Tendsto (fun (n : ℕ) => johnsonJ2 n (Asymptotics.shellWeight a n) (Asymptotics.complementDegree g n) / ↑n) Filter.atTop (nhds ((1 - a) / 2 - g))

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonJ_ratio {u : ℝ} (hu : 0 < u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonJ n (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n) / ↑n) Filter.atTop (nhds ((1 - 2 * u) / 2))

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

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonSigma_ratio {a b g : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) (hb : 0 ≤ b) (hg : 0 ≤ g) : Filter.Tendsto (fun (n : ℕ) => johnsonSigma n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) / ↑n) Filter.atTop (nhds ((1 - 2 * b - 2 * g) / 2))

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonDelta_ratio {a b g : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1) (hb : 0 ≤ b) (hg : 0 ≤ g) : Filter.Tendsto (fun (n : ℕ) => johnsonDelta n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) / ↑n) Filter.atTop (nhds (centeredEta a b g / 2))

theorem MetricCodes.Johnson.SpectralAsymptotics.johnsonMu_div_eq_normalized (n w p q j : ℕ) (hn : 0 < n) (hj : johnsonJ n j ≠ 0) (hj' : johnsonJ n j + 1 ≠ 0) : johnsonMu n w p q j / ↑n = MetricCodes.Johnson.SpectralAsymptotics.normalizedMu✝ (johnsonJ1 w p / ↑n) (johnsonJ2 n w q / ↑n) (johnsonJ n j / ↑n) (johnsonM n w / ↑n) (1 / ↑n)

theorem MetricCodes.Johnson.SpectralAsymptotics.normalizedMu_zero (a b g u : ℝ) (hz : 1 - 2 * u ≠ 0) : MetricCodes.Johnson.SpectralAsymptotics.normalizedMu✝ (a / 2 - b) ((1 - a) / 2 - g) ((1 - 2 * u) / 2) ((1 - 2 * a) / 2) 0 = MetricCodes.Johnson.SpectralAsymptotics.muLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonMu_div {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonMu n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n) / ↑n) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.muLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.johnsonDiagonal_eq_normalized (n w p q j : ℕ) (hn : 0 < n) (hw : 0 < w) (hwn : w < n) (hj : 0 < johnsonJ n j) : johnsonDiagonal n w p q j = MetricCodes.Johnson.SpectralAsymptotics.normalizedDiagonal✝ (johnsonJ1 w p / ↑n) (johnsonJ2 n w q / ↑n) (johnsonJ n j / ↑n) (johnsonM n w / ↑n) (1 / ↑n) (↑w / ↑n) (↑(n - w) / ↑n)

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonDiagonal {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonDiagonal n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n)) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.normalizedNu_scale (N J M eta sigma : ℝ) (hN : 0 < N) (hstep : 0 < 2 * J - 1) : √((J ^ 2 - M ^ 2) * (J ^ 2 - eta ^ 2) * ((sigma + 1) ^ 2 - J ^ 2)) / (2 * J * √((2 * J - 1) * (2 * J + 1))) / N = MetricCodes.Johnson.SpectralAsymptotics.normalizedNu✝ (J / N) (M / N) (eta / N) (sigma / N) (1 / N)

theorem MetricCodes.Johnson.SpectralAsymptotics.johnsonNu_div_eq_normalized (n w p q j : ℕ) (hn : 0 < n) (hstep : 0 < 2 * johnsonJ n j - 1) : johnsonNu n w p q j / ↑n = MetricCodes.Johnson.SpectralAsymptotics.normalizedNu✝ (johnsonJ n j / ↑n) (johnsonM n w / ↑n) (johnsonDelta n w p q / ↑n) (johnsonSigma n w p q / ↑n) (1 / ↑n)

theorem MetricCodes.Johnson.SpectralAsymptotics.normalizedNu_zero (a b g u : ℝ) (hz : 0 < 1 - 2 * u) : MetricCodes.Johnson.SpectralAsymptotics.normalizedNu✝ ((1 - 2 * u) / 2) ((1 - 2 * a) / 2) (centeredEta a b g / 2) ((1 - 2 * b - 2 * g) / 2) 0 = MetricCodes.Johnson.SpectralAsymptotics.nuLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonNu_div {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonNu n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n) / ↑n) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.nuLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonEdge {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonEdge n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n)) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.edgeLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.zeroFibreParameters {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : AsymptoticParameters d a 0 0 u

theorem MetricCodes.Johnson.SpectralAsymptotics.spectralLimit_eq_hatted {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : spectralLimit a b g u = MetricCodes.Johnson.SpectralAsymptotics.hattedDiagonalLimit✝ a b g u + 2 * MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit_pos {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : 0 < MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit_zero_eq {d a b g u : ℝ} (_h : AsymptoticParameters d a b g u) : MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit✝ a 0 0 u = (1 - 2 * a) ^ 2 * (1 - (1 - 2 * u) ^ 2) / ((1 - 2 * u) ^ 2 * (1 - (1 - 2 * a) ^ 2))

theorem MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit_zero_pos {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : 0 < MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit✝ a 0 0 u

theorem MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit_sq_div_zero {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit✝ a b g u ^ 2 / MetricCodes.Johnson.SpectralAsymptotics.diagonalLimit✝ a 0 0 u = MetricCodes.Johnson.SpectralAsymptotics.hattedDiagonalLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.edgeLimit_zero_eq {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : MetricCodes.Johnson.SpectralAsymptotics.edgeLimit✝ a 0 0 u = ((1 - 2 * u) ^ 2 - (1 - 2 * a) ^ 2) * √(1 - (1 - 2 * u) ^ 2) / (2 * (1 - 2 * u) ^ 2 * (1 - (1 - 2 * a) ^ 2))

theorem MetricCodes.Johnson.SpectralAsymptotics.edgeLimit_zero_pos {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : 0 < MetricCodes.Johnson.SpectralAsymptotics.edgeLimit✝ a 0 0 u

theorem MetricCodes.Johnson.SpectralAsymptotics.edgeLimit_sq_div_zero {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : MetricCodes.Johnson.SpectralAsymptotics.edgeLimit✝ a b g u ^ 2 / MetricCodes.Johnson.SpectralAsymptotics.edgeLimit✝ a 0 0 u = MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit✝ a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonHattedDiagonal {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonHattedDiagonal n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n)) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.hattedDiagonalLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_johnsonHattedEdge {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => johnsonHattedEdge n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (MetricCodes.Johnson.SpectralAsymptotics.terminalIndex✝ u r n)) Filter.atTop (nhds (MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit✝ a b g u))

theorem MetricCodes.Johnson.SpectralAsymptotics.tridiagonal_quadratic_sum (d : ℕ) (b c v : ℕ → ℝ) : ∑ i ∈ Finset.range (d + 1), ∑ j ∈ Finset.range (d + 1), (if i = j then b i else if i + 1 = j then c i else if j + 1 = i then c j else 0) * v j * v i = ∑ i ∈ Finset.range (d + 1), b i * v i ^ 2 + 2 * ∑ i ∈ Finset.range d, c i * v i * v (i + 1)

theorem MetricCodes.Johnson.SpectralAsymptotics.terminal_indicator_diagonal_sum (d m : ℕ) (hm : m ≤ d) (b : ℕ → ℝ) : ∑ i ∈ Finset.range (d + 1), b i * Hamming.terminalIndicator d m i ^ 2 = ∑ r ∈ Finset.range (m + 1), b (d - m + r)

def MetricCodes.Johnson.SpectralAsymptotics.terminalVector (p q L m : ℕ) : Space p q L

The terminal vector used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.SpectralAsymptotics.terminalVector p q L m = MetricCodes.Hamming.terminalVector (p + q) L m

theorem MetricCodes.Johnson.SpectralAsymptotics.terminalVector_ne_zero (p q L m : ℕ) : terminalVector p q L m ≠ 0

theorem MetricCodes.Johnson.SpectralAsymptotics.terminalVector_norm_sq (p q L m : ℕ) (hm : m ≤ L - (p + q)) : ‖terminalVector p q L m‖ ^ 2 = ↑m + 1

theorem MetricCodes.Johnson.SpectralAsymptotics.terminalVector_inner (n w p q L m : ℕ) (hfirst : p + q ≤ L) (hm : m ≤ L - (p + q)) : inner ℝ ((operator n w p q L) (terminalVector p q L m)) (terminalVector p q L m) = ∑ r ∈ Finset.range (m + 1), johnsonHattedDiagonal n w p q (L - m + r) + 2 * ∑ r ∈ Finset.range m, johnsonHattedEdge n w p q (L - m + r)

theorem MetricCodes.Johnson.SpectralAsymptotics.terminalVector_rayleigh (n w p q L m : ℕ) (hfirst : p + q ≤ L) (hm : m ≤ L - (p + q)) : rayleigh n w p q L (terminalVector p q L m) = (∑ r ∈ Finset.range (m + 1), johnsonHattedDiagonal n w p q (L - m + r) + 2 * ∑ r ∈ Finset.range m, johnsonHattedEdge n w p q (L - m + r)) / (↑m + 1)

theorem MetricCodes.Johnson.SpectralAsymptotics.terminal_rayleigh_le_top (n w p q L m : ℕ) (hfirst : p + q ≤ L) (hm : m ≤ L - (p + q)) : (∑ r ∈ Finset.range (m + 1), johnsonHattedDiagonal n w p q (L - m + r) + 2 * ∑ r ∈ Finset.range m, johnsonHattedEdge n w p q (L - m + r)) / (↑m + 1) ≤ topEigenvalue n w p q L

theorem MetricCodes.Johnson.SpectralAsymptotics.tendsto_terminalRayleigh {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) (m : ℕ) : Filter.Tendsto (MetricCodes.Johnson.SpectralAsymptotics.terminalRayleigh✝ a b g u m) Filter.atTop (nhds (((↑m + 1) * MetricCodes.Johnson.SpectralAsymptotics.hattedDiagonalLimit✝ a b g u + 2 * ↑m * MetricCodes.Johnson.SpectralAsymptotics.hattedEdgeLimit✝ a b g u) / (↑m + 1)))

theorem MetricCodes.Johnson.SpectralAsymptotics.terminalRayleigh_le_top (a b g u : ℝ) (m n : ℕ) (hfit : Asymptotics.supportDegree b n + Asymptotics.complementDegree g n + m ≤ Asymptotics.terminalDegree u n) : MetricCodes.Johnson.SpectralAsymptotics.terminalRayleigh✝ a b g u m n ≤ topEigenvalue n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n)

theorem MetricCodes.Johnson.SpectralAsymptotics.eventually_topEigenvalue_gt {d a b g u s : ℝ} (h : AsymptoticParameters d a b g u) (hs : s < spectralLimit a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, s < topEigenvalue n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n)

noncomputable def MetricCodes.Johnson.SpectralAsymptotics.spectralGap (d a b g u : ℝ) : ℝ

The spectral gap used in the Johnson-code argument.

Equations

• MetricCodes.Johnson.SpectralAsymptotics.spectralGap d a b g u = (MetricCodes.Johnson.spectralLimit a b g u - MetricCodes.Johnson.asymptoticThreshold d a) / 4

theorem MetricCodes.Johnson.SpectralAsymptotics.spectralGap_pos {d a b g u : ℝ} (h : Feasible d a b g u) : 0 < spectralGap d a b g u

theorem MetricCodes.Johnson.SpectralAsymptotics.eventually_spectralGap_lt {d a b g u : ℝ} (h : Feasible d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, spectralGap d a b g u < topEigenvalue n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n) - threshold n (Asymptotics.shellWeight a n) ⌈d * ↑n⌉₊

theorem MetricCodes.Johnson.SpectralAsymptotics.asymptoticThreshold_lt_one {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : asymptoticThreshold d a < 1

theorem MetricCodes.Johnson.SpectralAsymptotics.eventually_one_sub_threshold_lt {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, 1 - threshold n (Asymptotics.shellWeight a n) ⌈d * ↑n⌉₊ < 2 - asymptoticThreshold d a

theorem MetricCodes.Johnson.Rate.certificateConstant_pos {d a b g u : ℝ} (h : Feasible d a b g u) : 0 < MetricCodes.Johnson.Rate.certificateConstant✝ d a b g u

theorem MetricCodes.Johnson.Rate.exists_zero_fibre_feasible {d : ℝ} (hd : 0 < d) (hdhalf : d < 1 / 2) : ∃ (a : ℝ) (u : ℝ), Feasible d a 0 0 u

theorem MetricCodes.Johnson.Rate.rateSet_nonempty_of_interior {d : ℝ} (hd : 0 < d) (hdhalf : d < 1 / 2) : (rateSet d).Nonempty

theorem MetricCodes.Johnson.Rate.eventually_strict_weight_half {d a b g u : ℝ} (h : AsymptoticParameters d a b g u) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * Asymptotics.shellWeight a n < n

theorem MetricCodes.Johnson.Rate.binaryRate_le_shellRate_of_projectionGrams {d a b g u : ℝ} (h : Feasible d a b g u) (hdata : ∀ᶠ (n : ℕ) in Filter.atTop, Nonempty (ProjectionGram n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n))) : Hamming.binaryRate d ≤ shellRate a b g u

theorem MetricCodes.Johnson.Rate.binaryRate_le_variationalRate_of_projectionGrams {d : ℝ} (hd : 0 < d) (hdhalf : d < 1 / 2) (hdata : ∀ (a b g u : ℝ), Feasible d a b g u → ∀ᶠ (n : ℕ) in Filter.atTop, Nonempty (ProjectionGram n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n))) : Hamming.binaryRate d ≤ variationalRate d

theorem MetricCodes.Johnson.Rate.binaryRate_le_combinedVariationalRate_of_projectionGrams {d : ℝ} (hd : 0 < d) (hdhalf : d < 1 / 2) (hdata : ∀ (a b g u : ℝ), Feasible d a b g u → ∀ᶠ (n : ℕ) in Filter.atTop, Nonempty (ProjectionGram n (Asymptotics.shellWeight a n) (Asymptotics.supportDegree b n) (Asymptotics.complementDegree g n) (Asymptotics.terminalDegree u n))) : Hamming.binaryRate d ≤ combinedVariationalRate d

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

theorem MetricCodes.Johnson.binaryRate_le_combinedVariationalRate {d : ℝ} (hd : 0 < d) (hdhalf : d < 1 / 2) : Hamming.binaryRate d ≤ combinedVariationalRate d

noncomputable def MetricCodes.Numerics.logSeriesLower (x : ℝ) (m : ℕ) : ℝ

The log series lower used in the metric-code argument.

Equations

• MetricCodes.Numerics.logSeriesLower x m = 2 * ∑ i ∈ Finset.range m, x ^ (2 * i + 1) / (2 * ↑i + 1)

noncomputable def MetricCodes.Numerics.logSeriesUpper (x : ℝ) (m : ℕ) : ℝ

The log series upper used in the metric-code argument.

Equations

• MetricCodes.Numerics.logSeriesUpper x m = MetricCodes.Numerics.logSeriesLower x m + 2 * (x ^ (2 * m + 1) / (1 - x ^ 2))

theorem MetricCodes.Numerics.log_ratio_lower {x : ℝ} (hx : 0 ≤ x) (hx' : x < 1) (m : ℕ) : logSeriesLower x m ≤ Real.log ((1 + x) / (1 - x))

theorem MetricCodes.Numerics.log_ratio_upper {x : ℝ} (hx : 0 ≤ x) (hx' : x < 1) (m : ℕ) : Real.log ((1 + x) / (1 - x)) ≤ logSeriesUpper x m

theorem MetricCodes.Numerics.log_interval_of_series {r x lo hi : ℝ} (m : ℕ) (hx : 0 ≤ x) (hx' : x < 1) (hr : (1 + x) / (1 - x) = r) (hlo : lo < logSeriesLower x m) (hhi : logSeriesUpper x m < hi) : lo < Real.log r ∧ Real.log r < hi

theorem MetricCodes.Numerics.log_two_interval : 693147180559945309 / 10 ^ 18 < Real.log 2 ∧ Real.log 2 < 693147180559945310 / 10 ^ 18

theorem MetricCodes.Numerics.log_kissing_one_add_a_interval : 82226264808038924 / 10 ^ 18 < Real.log (1 + MetricCodes.Numerics.kissingA✝) ∧ Real.log (1 + MetricCodes.Numerics.kissingA✝) < 82226264808038925 / 10 ^ 18

theorem MetricCodes.Numerics.log_kissing_scaled_a_interval : 315703048970999865 / 10 ^ 18 < Real.log (16 * MetricCodes.Numerics.kissingA✝) ∧ Real.log (16 * MetricCodes.Numerics.kissingA✝) < 315703048970999866 / 10 ^ 18

theorem MetricCodes.Numerics.log_kissing_one_add_b_interval : 3695990739373266 / 10 ^ 18 < Real.log (1 + MetricCodes.Numerics.kissingB✝) ∧ Real.log (1 + MetricCodes.Numerics.kissingB✝) < 3695990739373267 / 10 ^ 18

theorem MetricCodes.Numerics.log_kissing_inverse_scaled_b_interval : 53480621756332520 / 10 ^ 18 < Real.log (1 / (256 * MetricCodes.Numerics.kissingB✝)) ∧ Real.log (1 / (256 * MetricCodes.Numerics.kissingB✝)) < 53480621756332521 / 10 ^ 18

theorem MetricCodes.Numerics.kissing_sqrt_upper : √(MetricCodes.Numerics.kissingA✝ * (1 + MetricCodes.Numerics.kissingA✝)) < 30503471040898065 / 10 ^ 17

theorem MetricCodes.Numerics.kissing_spectral_certificate : 1 / 2 < 2 * Gamma MetricCodes.Numerics.kissingA✝ MetricCodes.Numerics.kissingB✝

theorem MetricCodes.Numerics.log_kissing_a : Real.log MetricCodes.Numerics.kissingA✝ = Real.log (16 * MetricCodes.Numerics.kissingA✝) - 4 * Real.log 2

theorem MetricCodes.Numerics.log_kissing_b : Real.log MetricCodes.Numerics.kissingB✝ = -8 * Real.log 2 - Real.log (1 / (256 * MetricCodes.Numerics.kissingB✝))

theorem MetricCodes.Numerics.kissing_entropy_certificate : sphericalEntropy MetricCodes.Numerics.kissingA✝ - sphericalEntropy MetricCodes.Numerics.kissingB✝ < 0.397305601680

theorem MetricCodes.Spherical.sphericalEntropy_continuous : Continuous sphericalEntropy

theorem MetricCodes.Spherical.hasDerivAt_sphericalEntropy {u : ℝ} (hu : 0 < u) : HasDerivAt sphericalEntropy (Real.logb 2 ((1 + u) / u)) u

theorem MetricCodes.Spherical.sphericalEntropy_strictMono : StrictMonoOn sphericalEntropy (Set.Ici 0)

theorem MetricCodes.Spherical.sphericalEntropy_sub_nonneg {a b : ℝ} (hb : 0 ≤ b) (hba : b ≤ a) : 0 ≤ sphericalEntropy a - sphericalEntropy b

def MetricCodes.Spherical.Feasible (s a b : ℝ) : Prop

The feasible used in the spherical-code argument.

Equations

• MetricCodes.Spherical.Feasible s a b = (0 < b ∧ b < a ∧ s < 2 * MetricCodes.Gamma a b)

def MetricCodes.Spherical.rateSet (s : ℝ) : Set ℝ

The rate set used in the spherical-code argument.

Equations

• MetricCodes.Spherical.rateSet s = {r : ℝ | ∃ (a : ℝ) (b : ℝ), MetricCodes.Spherical.Feasible s a b ∧ r = MetricCodes.sphericalEntropy a - MetricCodes.sphericalEntropy b}

noncomputable def MetricCodes.Spherical.variationalRate (s : ℝ) : ℝ

The variational rate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.variationalRate s = sInf (MetricCodes.Spherical.rateSet s)

theorem MetricCodes.Spherical.rateSet_bddBelow (s : ℝ) : BddBelow (rateSet s)

theorem MetricCodes.Spherical.variationalRate_le_of_feasible {s a b : ℝ} (h : Feasible s a b) : variationalRate s ≤ sphericalEntropy a - sphericalEntropy b

theorem MetricCodes.Spherical.Gamma_zero {a : ℝ} (ha : 0 < a) : Gamma a 0 = √(a * (1 + a)) / (1 + 2 * a)

theorem MetricCodes.Spherical.classicalThreshold_spectral {s : ℝ} (hs : 0 < s) (hs' : s < 1) : 2 * Gamma (classicalThreshold s) 0 = s

def MetricCodes.Spherical.sphericalImprovementPath (a b : ℝ) : ℝ

The spherical improvement path used in the spherical-code argument.

Equations

• MetricCodes.Spherical.sphericalImprovementPath a b = a + (4 * a + 3) * b

theorem MetricCodes.Spherical.sphericalImprovementSlope_gt_one {a : ℝ} (ha : 0 < a) : 1 < 4 * a + 3

theorem MetricCodes.Spherical.sphericalSpectralMarginPolynomial_factor (a c b : ℝ) : (((a + c * b) * (1 + (a + c * b)) - b * (1 + b)) * (1 + 2 * a)) ^ 2 - a * (1 + a) * (1 + 2 * (a + c * b)) ^ 2 * ((a + c * b) * (1 + (a + c * b))) = b * MetricCodes.Spherical.sphericalSpectralMarginPolynomial✝ a c b

theorem MetricCodes.Spherical.sphericalSpectralMarginPolynomial_continuous (a c : ℝ) : Continuous (MetricCodes.Spherical.sphericalSpectralMarginPolynomial✝ a c)

theorem MetricCodes.Spherical.sphericalSpectralMarginPolynomial_improvement_zero (a : ℝ) : MetricCodes.Spherical.sphericalSpectralMarginPolynomial✝ a (4 * a + 3) 0 = a * (1 + a) * (1 + 2 * a)

theorem MetricCodes.Spherical.eventually_Gamma_improvement {a : ℝ} (ha : 0 < a) : ∀ᶠ (b : ℝ) in nhdsWithin 0 (Set.Ioi 0), Gamma a 0 < Gamma (sphericalImprovementPath a b) b

theorem MetricCodes.Spherical.neg_mul_logb_le_sphericalEntropy {b : ℝ} (hb : 0 ≤ b) : b * -Real.logb 2 b ≤ sphericalEntropy b

theorem MetricCodes.Spherical.eventually_sphericalEntropy_improvement {a : ℝ} (ha : 0 < a) : ∀ᶠ (b : ℝ) in nhdsWithin 0 (Set.Ioi 0), sphericalEntropy (sphericalImprovementPath a b) - sphericalEntropy b < sphericalEntropy a

theorem MetricCodes.Spherical.exists_strict_improving_spherical_feasible {s : ℝ} (hs : 0 < s) (hs' : s < 1) : ∃ (a : ℝ) (b : ℝ), Feasible s a b ∧ sphericalEntropy a - sphericalEntropy b < sphericalEntropy (classicalThreshold s)

theorem MetricCodes.Spherical.classicalThreshold_continuousAt {s : ℝ} (hs : -1 < s) (hs' : s < 1) : ContinuousAt classicalThreshold s

theorem MetricCodes.Spherical.sphericalEntropy_eq_logb_add_mul_logb {a : ℝ} (ha : 0 < a) : sphericalEntropy a = Real.logb 2 (1 + a) + a * Real.logb 2 ((1 + a) / a)

noncomputable def MetricCodes.Spherical.HigherHierarchy.spectralAtom (u : ℝ) : ℝ

The spectral atom used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.spectralAtom u = √(u * (1 + u)) / (1 + 2 * u)

def MetricCodes.Spherical.HigherHierarchy.Interlacing {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : Prop

The interlacing used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Interlacing a b = (0 ≤ a (Fin.last r) ∧ ∀ (i : Fin r), a i.castSucc > b i ∧ b i > a i.succ)

def MetricCodes.Spherical.HigherHierarchy.lagrangeNumerator {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (ℓ : Fin (r + 1)) : ℝ

The lagrange numerator used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.lagrangeNumerator a b ℓ = ∏ m : Fin r, (a ℓ * (1 + a ℓ) - b m * (1 + b m))

def MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator {r : ℕ} (a : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ℝ

The lagrange denominator used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator a ℓ = ∏ m : Fin r, (a ℓ * (1 + a ℓ) - a (ℓ.succAbove m) * (1 + a (ℓ.succAbove m)))

noncomputable def MetricCodes.Spherical.HigherHierarchy.lagrangeWeight {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (ℓ : Fin (r + 1)) : ℝ

The lagrange weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.lagrangeWeight a b ℓ = MetricCodes.Spherical.HigherHierarchy.lagrangeNumerator a b ℓ / MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator a ℓ

noncomputable def MetricCodes.Spherical.HigherHierarchy.Gamma {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : ℝ

The gamma used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Gamma a b = ∑ ℓ : Fin (r + 1), MetricCodes.Spherical.HigherHierarchy.lagrangeWeight a b ℓ * MetricCodes.Spherical.HigherHierarchy.spectralAtom (a ℓ)

noncomputable def MetricCodes.Spherical.HigherHierarchy.Phi {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : ℝ

The phi used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Phi a b = ∑ ℓ : Fin (r + 1), MetricCodes.sphericalEntropy (a ℓ) - ∑ m : Fin r, MetricCodes.sphericalEntropy (b m)

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.strictAnti_ambient {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : StrictAnti a

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.ambient_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin (r + 1)) : 0 ≤ a i

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.stabilizer_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin r) : 0 < b i

theorem MetricCodes.Spherical.HigherHierarchy.quadraticCoordinate_strictMonoOn : StrictMonoOn (fun (u : ℝ) => u * (1 + u)) (Set.Ici 0)

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.quadratic_injective {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : Function.Injective fun (i : Fin (r + 1)) => a i * (1 + a i)

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator_eq_prod_erase {r : ℕ} (a : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : lagrangeDenominator a ℓ = ∏ j ∈ Finset.univ.erase ℓ, (a ℓ * (1 + a ℓ) - a j * (1 + a j))

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.lagrangeDenominator_ne_zero {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (ℓ : Fin (r + 1)) : lagrangeDenominator a ℓ ≠ 0

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.lagrangeFactor_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (ℓ : Fin (r + 1)) (m : Fin r) : 0 < (a ℓ * (1 + a ℓ) - b m * (1 + b m)) / (a ℓ * (1 + a ℓ) - a (ℓ.succAbove m) * (1 + a (ℓ.succAbove m)))

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.lagrangeWeight_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (ℓ : Fin (r + 1)) : 0 < lagrangeWeight a b ℓ

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.lagrangeWeight_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (ℓ : Fin (r + 1)) : 0 ≤ lagrangeWeight a b ℓ

theorem MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial_monic {r : ℕ} (b : Fin r → ℝ) : (MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial✝ b).Monic

theorem MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial_natDegree {r : ℕ} (b : Fin r → ℝ) : (MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial✝ b).natDegree = r

theorem MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial_eval {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (ℓ : Fin (r + 1)) : Polynomial.eval (a ℓ * (1 + a ℓ)) (MetricCodes.Spherical.HigherHierarchy.stabilizerPolynomial✝ b) = lagrangeNumerator a b ℓ

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.sum_lagrangeWeight {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : ∑ ℓ : Fin (r + 1), lagrangeWeight a b ℓ = 1

theorem MetricCodes.Spherical.HigherHierarchy.spectralAtom_nonneg {u : ℝ} (hu : 0 ≤ u) : 0 ≤ spectralAtom u

theorem MetricCodes.Spherical.HigherHierarchy.Arcsine.beta_half_half_eq_pi : ProbabilityTheory.beta (1 / 2) (1 / 2) = Real.pi

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineIntegral.integral_inv_add_mul_cos (a b : ℝ) (h : |b| < a) : ∫ (θ : ℝ) in 0..Real.pi, (a + b * Real.cos θ)⁻¹ = Real.pi / √(a ^ 2 - b ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.betaPDFReal_half_half_eq (u : ℝ) (hu₀ : 0 < u) (hu₁ : u < 1) : ProbabilityTheory.betaPDFReal (1 / 2) (1 / 2) u = 1 / Real.pi * (√(u * (1 - u)))⁻¹

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.integral_beta_half_half_eq_integral_measureT (f : ℝ → ℝ) : ∫ (u : ℝ), f u ∂ProbabilityTheory.betaMeasure (1 / 2) (1 / 2) = 1 / Real.pi * ∫ (z : ℝ), f ((z + 1) / 2) ∂Polynomial.Chebyshev.measureT

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.integral_betaMap_half_half_eq_integral_cos (f : ℝ → ℝ) (hf : Measurable f) : ∫ (t : ℝ), f t ∂MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)) = 1 / Real.pi * ∫ (θ : ℝ) in 0..Real.pi, f ((Real.cos θ + 1) / 8)

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.betaMap_half_half_ae_pos : ∀ᵐ (t : ℝ) ∂MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)), 0 < t

instance MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.betaMap_half_half_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)))

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.arcsine_stieltjes_integrable {x : ℝ} (hx : 0 ≤ x) : MeasureTheory.Integrable (fun (t : ℝ) => x / (x + t)) (MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)))

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.arcsine_integral_x_div_add {x : ℝ} (hx : 0 < x) : ∫ (t : ℝ), x / (x + t) ∂MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)) = √(x / (x + 1 / 4))

theorem MetricCodes.Spherical.HigherHierarchy.ArcsineTransform.arcsine_integral_self_div_add {x : ℝ} (hx : 0 ≤ x) : ∫ (t : ℝ), t / (t + x) ∂MeasureTheory.Measure.map (fun (t : ℝ) => t / 4) (ProbabilityTheory.betaMeasure (1 / 2) (1 / 2)) = 1 - √(x / (x + 1 / 4))

noncomputable def MetricCodes.Spherical.HigherHierarchyChebyshev.zero (R : ℝ) (N j : ℕ) : ℝ

The zero used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyChebyshev.zero R N j = R / 2 * (1 + Real.cos (MetricCodes.Spherical.HigherHierarchyChebyshev.zeroAngle✝ N j))

noncomputable def MetricCodes.Spherical.HigherHierarchyChebyshev.stabilizer (R : ℝ) (r : ℕ) (i : Fin r) : ℝ

The stabilizer used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyChebyshev.stabilizer R r i = (√(1 + 4 * MetricCodes.Spherical.HigherHierarchyChebyshev.zero R (r + 1) (↑i + 1)) - 1) / 2

def MetricCodes.Spherical.HigherHierarchy.Numerics.kissingAmbient : Fin 3 → ℝ

The kissing ambient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Numerics.kissingAmbient = ![90531e-6, 565957168637484e-18, 249433171106134e-20]

def MetricCodes.Spherical.HigherHierarchy.Numerics.kissingStabilizer : Fin 2 → ℝ

The kissing stabilizer used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Numerics.kissingStabilizer = ![693131464159807e-17, 438056170666568e-19]

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissingAmbient_apply (i : Fin 3) : kissingAmbient i = if ↑i = 0 then 90531e-6 else if ↑i = 1 then 565957168637484e-18 else 249433171106134e-20

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissingStabilizer_apply (i : Fin 2) : kissingStabilizer i = if ↑i = 0 then 693131464159807e-17 else 438056170666568e-19

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.succAbove_three_20 : Fin.succAbove 2 0 = 0

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.succAbove_three_21 : Fin.succAbove 2 1 = 1

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissing_interlacing : Interlacing kissingAmbient kissingStabilizer

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissing_sqrt_lower : 0.31420830982168 < √(kissingAmbient 0 * (1 + kissingAmbient 0)) ∧ 2379658538854e-14 < √(kissingAmbient 1 * (1 + kissingAmbient 1)) ∧ 157934731226e-14 < √(kissingAmbient 2 * (1 + kissingAmbient 2))

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissing_spectral_certificate : 212e-8 < 2 * Gamma kissingAmbient kissingStabilizer - 1 / 2

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.rational_log_lower {r lo : ℝ} (hr : 1 ≤ r) (m : ℕ) (hlo : lo < Numerics.logSeriesLower ((r - 1) / (r + 1)) m) : lo < Real.log r

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.rational_log_upper {r hi : ℝ} (hr : 1 ≤ r) (m : ℕ) (hhi : Numerics.logSeriesUpper ((r - 1) / (r + 1)) m < hi) : Real.log r < hi

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.log_scaled_pow_two {u : ℝ} (hu : u ≠ 0) (k : ℕ) : Real.log u = Real.log (2 ^ k * u) - ↑k * Real.log 2

theorem MetricCodes.Spherical.HigherHierarchy.Numerics.kissing_entropy_certificate : Phi kissingAmbient kissingStabilizer < 0.396605

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.Phi_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : 0 ≤ Phi a b

def MetricCodes.Spherical.HigherHierarchy.hierarchyRateSet (s : ℝ) : Set ℝ

The hierarchy rate set used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate (s : ℝ) : ℝ

The hierarchy variational rate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate s = sInf (MetricCodes.Spherical.HigherHierarchy.hierarchyRateSet s)

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyRateSet_bddBelow (s : ℝ) : BddBelow (hierarchyRateSet s)

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_of_feasible {r : ℕ} {s : ℝ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hgap : s < 2 * Gamma a b) : hierarchyVariationalRate s ≤ Phi a b

noncomputable def MetricCodes.Spherical.HigherHierarchy.stieltjesPhase {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (t : ℝ) : ℝ

The stieltjes phase used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchy.stieltjesPhaseProduct {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (t : ℝ) : ℝ

The stieltjes phase product used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.stieltjesPhaseProduct a b t = (t * ∏ i : Fin r, (t + b i * (1 + b i))) / ∏ i : Fin (r + 1), (t + a i * (1 + a i))

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.ambient_quadratic_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin (r + 1)) : 0 ≤ a i * (1 + a i)

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.stabilizer_quadratic_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin r) : 0 < b i * (1 + b i)

theorem MetricCodes.Spherical.HigherHierarchy.integral_inv_add_eq_log_div {t p q : ℝ} (hp : 0 < t + p) (hq : 0 < t + q) : ∫ (u : ℝ) in p..q, (t + u)⁻¹ = Real.log ((t + q) / (t + p))

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPhase_eq_log_sum {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : stieltjesPhase a b t = Real.log ((t + a (Fin.last r) * (1 + a (Fin.last r))) / t) + ∑ i : Fin r, Real.log ((t + a i.castSucc * (1 + a i.castSucc)) / (t + b i * (1 + b i)))

theorem MetricCodes.Spherical.HigherHierarchy.exp_neg_stieltjesPhase_eq_product {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : Real.exp (-stieltjesPhase a b t) = stieltjesPhaseProduct a b t

theorem MetricCodes.Spherical.HigherHierarchy.polynomial_partialFraction {r : ℕ} {x : Fin (r + 1) → ℝ} (hx : Function.Injective x) (P : Polynomial ℝ) (hdegree : P.degree < ↑Finset.univ.card) {z : ℝ} (hz : ∀ (i : Fin (r + 1)), z ≠ x i) : Polynomial.eval z P / ∏ i : Fin (r + 1), (z - x i) = ∑ i : Fin (r + 1), (Polynomial.eval (x i) P / ∏ j ∈ Finset.univ.erase i, (x i - x j)) / (z - x i)

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPartialFraction {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : (∏ i : Fin r, (t + b i * (1 + b i))) / ∏ i : Fin (r + 1), (t + a i * (1 + a i)) = ∑ i : Fin (r + 1), lagrangeWeight a b i / (t + a i * (1 + a i))

theorem MetricCodes.Spherical.HigherHierarchy.exp_neg_stieltjesPhase_eq_lagrange_sum {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : Real.exp (-stieltjesPhase a b t) = ∑ i : Fin (r + 1), lagrangeWeight a b i * (t / (t + a i * (1 + a i)))

theorem MetricCodes.Spherical.HigherHierarchy.quadratic_spectralAtom_identity {u : ℝ} (hu : 0 ≤ u) : √(u * (1 + u) / (u * (1 + u) + 1 / 4)) = 2 * spectralAtom u

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesKernel_integrable (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {x : ℝ} (hx : 0 ≤ x) (hpositive : ∀ᵐ (t : ℝ) ∂μ, 0 < t) : MeasureTheory.Integrable (fun (t : ℝ) => t / (t + x)) μ

theorem MetricCodes.Spherical.HigherHierarchy.integral_exp_neg_stieltjesPhase_eq_one_sub_two_Gamma {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hpositive : ∀ᵐ (t : ℝ) ∂μ, 0 < t) (hstieltjes : ∀ (i : Fin (r + 1)), ∫ (t : ℝ), t / (t + a i * (1 + a i)) ∂μ = 1 - 2 * spectralAtom (a i)) : ∫ (t : ℝ), Real.exp (-stieltjesPhase a b t) ∂μ = 1 - 2 * Gamma a b