Spherical-code hierarchy

General spectral bounds, localization, compactification, and strict hierarchy estimates.

theorem MetricCodes.Spherical.variationalRate_lt_classical {s : ℝ} (hs : 0 < s) (hs' : s < 1) : variationalRate s < sphericalEntropy (classicalThreshold s)

theorem MetricCodes.Spherical.rateSet_nonempty_of_interior {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (rateSet s).Nonempty

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

The longitudinal degree used in the spherical-code argument.

Equations

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

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

The transverse degree used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.GeneralSpectral.sphericalCode_bound_of_actual_harmonic_channels {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) {s : ℝ} (hs : s ≤ 1) (hgap : s < SpherePacking.Jacobi.topEigenvalue n k L) (C : SpherePacking.SphericalCode n s) : ↑C.points.card ≤ (1 - s) / (SpherePacking.Jacobi.topEigenvalue n k L - s) * (↑(SpherePacking.truncatedHarmonicDimension n k L) / ↑(SpherePacking.Gegenbauer.fibreDimension n k))

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

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

theorem MetricCodes.Spherical.GeneralSpectral.tendsto_longitudinalDegree_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (longitudinalDegree a) Filter.atTop Filter.atTop

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

theorem MetricCodes.Spherical.GeneralSpectral.normalizedCoefficient_eq_Gamma {a : ℝ} (ha : 0 < a) (b : ℝ) : SpherePacking.SpectralAsymptotics.normalizedCoefficient a b 0 = Gamma a b

theorem MetricCodes.Spherical.GeneralSpectral.tendsto_terminal_coefficient {a b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => SpherePacking.Gegenbauer.jacobiCoefficient n (transverseDegree b n) (longitudinalDegree a n - r)) Filter.atTop (nhds (Gamma a b))

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

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

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

Equations

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

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

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

theorem MetricCodes.Spherical.GeneralSpectral.eventually_topEigenvalue_gt {a b s : ℝ} (hb : 0 ≤ b) (hba : b < a) (hs : s < 2 * Gamma a b) : ∀ᶠ (n : ℕ) in Filter.atTop, s < SpherePacking.Jacobi.topEigenvalue n (transverseDegree b n) (longitudinalDegree a n)

noncomputable def MetricCodes.Spherical.GeneralSpectral.spectralGap (s a b : ℝ) : ℝ

The spectral gap used in the spherical-code argument.

Equations

• MetricCodes.Spherical.GeneralSpectral.spectralGap s a b = (2 * MetricCodes.Gamma a b - s) / 2

theorem MetricCodes.Spherical.GeneralSpectral.spectralGap_pos {s a b : ℝ} (h : s < 2 * Gamma a b) : 0 < spectralGap s a b

theorem MetricCodes.Spherical.GeneralSpectral.eventually_topEigenvalue_uniform_gap {a b s : ℝ} (hb : 0 ≤ b) (hba : b < a) (hs : s < 2 * Gamma a b) : ∀ᶠ (n : ℕ) in Filter.atTop, s + spectralGap s a b < SpherePacking.Jacobi.topEigenvalue n (transverseDegree b n) (longitudinalDegree a n)

noncomputable def MetricCodes.Spherical.GeneralSpectral.spectralPrefactor (s a b : ℝ) : ℝ

The spectral prefactor used in the spherical-code argument.

Equations

• MetricCodes.Spherical.GeneralSpectral.spectralPrefactor s a b = (1 - s) / MetricCodes.Spherical.GeneralSpectral.spectralGap s a b

theorem MetricCodes.Spherical.GeneralSpectral.spectralPrefactor_pos {s a b : ℝ} (hs : s < 1) (hgap : s < 2 * Gamma a b) : 0 < spectralPrefactor s a b

theorem MetricCodes.Spherical.GeneralSpectral.legacy_binaryEntropy_eq_sphericalEntropy (u : ℝ) : SpherePacking.NumericalCertificate.binaryEntropy u = sphericalEntropy u

theorem MetricCodes.Spherical.GeneralSpectral.eventually_sphericalCode_card_le_harmonicQuotient {s a b : ℝ} (hs : s < 1) (hb : 0 < b) (hba : b < a) (hspectral : s < 2 * Gamma a b) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card ≤ spectralPrefactor s a b * SpherePacking.harmonicDimensionQuotient a b n

theorem MetricCodes.Spherical.GeneralSpectral.tendsto_log_spectral_harmonicQuotient {s a b : ℝ} (hs : s < 1) (hb : 0 < b) (hba : b < a) (hspectral : s < 2 * Gamma a b) : Filter.Tendsto (fun (n : ℕ) => Real.log (spectralPrefactor s a b * SpherePacking.harmonicDimensionQuotient a b n) / ↑n / Real.log 2) Filter.atTop (nhds (sphericalEntropy a - sphericalEntropy b))

theorem MetricCodes.Spherical.GeneralSpectral.eventually_sphericalCode_card_lt_rpow {s a b r : ℝ} (hs : s < 1) (hb : 0 < b) (hba : b < a) (hspectral : s < 2 * Gamma a b) (hr : sphericalEntropy a - sphericalEntropy b < r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (r * ↑n)

def SpherePacking.SphericalCode.toCodes {n : ℕ} {s : ℝ} (C : SphericalCode n s) : MetricCodes.SphericalCode n s

The to codes used in the spherical-code argument.

Equations

• C.toCodes = { points := Finset.map (SpherePacking.attachedSphereEmbedding_metriccodes2_d60650ef✝ C) C.points.attach, inner_le := ⋯ }

def SpherePacking.SphericalCode.ofCodes {n : ℕ} {s : ℝ} (C : MetricCodes.SphericalCode n s) : SphericalCode n s

The of codes used in the spherical-code argument.

Equations

• SpherePacking.SphericalCode.ofCodes C = { points := Finset.map (SpherePacking.spherePointEmbedding_metriccodes2_d60650ef✝ n) C.points, unit_norm := ⋯, inner_le := ⋯ }

@[simp]

theorem SpherePacking.SphericalCode.toCodes_card {n : ℕ} {s : ℝ} (C : SphericalCode n s) : C.toCodes.points.card = C.points.card

@[simp]

theorem SpherePacking.SphericalCode.ofCodes_card {n : ℕ} {s : ℝ} (C : MetricCodes.SphericalCode n s) : (ofCodes C).points.card = C.points.card

noncomputable def SpherePacking.sphericalCodeNumber (n : ℕ) (s : ℝ) : ℕ∞

The spherical code number used in the spherical-code argument.

Equations

• SpherePacking.sphericalCodeNumber n s = ⨆ (C : SpherePacking.SphericalCode n s), ↑C.points.card

theorem SpherePacking.sphericalCode_card_le_number {n : ℕ} {s : ℝ} (C : SphericalCode n s) : ↑C.points.card ≤ sphericalCodeNumber n s

theorem SpherePacking.sphericalCodeNumber_eq_codes (n : ℕ) (s : ℝ) : sphericalCodeNumber n s = MetricCodes.sphericalCodeNumber n s

theorem SpherePacking.sphericalCodeNumber_lt_top {n : ℕ} {s : ℝ} (hs : s < 1) : sphericalCodeNumber n s < ⊤

theorem SpherePacking.exists_maximal_sphericalCode {n : ℕ} {s : ℝ} (hs : s < 1) : ∃ (C : SphericalCode n s), ↑C.points.card = sphericalCodeNumber n s

theorem MetricCodes.Spherical.MaximalCodeBounds.exists_sphericalCode_card_eq_number_toNat {n : ℕ} {s : ℝ} (hs : s < 1) : ∃ (C : SpherePacking.SphericalCode n s), C.points.card = (SpherePacking.sphericalCodeNumber n s).toNat

theorem MetricCodes.Spherical.MaximalCodeBounds.sphericalCodeNumber_toNat_lt_iff {n : ℕ} {s B : ℝ} (hs : s < 1) : ↑(SpherePacking.sphericalCodeNumber n s).toNat < B ↔ ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < B

theorem MetricCodes.Spherical.HigherHierarchy.exists_oneRow_certificate_better_than_levelZero {s a : ℝ} (ha : 0 < a) (hspectral : s < 2 * spectralAtom a) : ∃ (A : ℝ) (b : ℝ), 0 < b ∧ b < A ∧ s < 2 * MetricCodes.Gamma A b ∧ sphericalEntropy A - sphericalEntropy b < sphericalEntropy a

theorem MetricCodes.Spherical.HigherHierarchy.eventually_sphericalCode_card_lt_levelZero {s : ℝ} (hs : 0 < s) (hs' : s < 1) (a : Fin 1 → ℝ) (b : Fin 0 → ℝ) (hinterlacing : Interlacing a b) (hspectral : s < 2 * Gamma a b) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (Phi a b * ↑n)

theorem MetricCodes.Spherical.zero_fibre_spectral_iff_classicalThreshold_lt {s a : ℝ} (hs : 0 < s) (hs' : s < 1) (ha : 0 < a) : s < 2 * Gamma a 0 ↔ classicalThreshold s < a

theorem MetricCodes.Spherical.boundaryQuadratic_pos_iff_classicalThreshold_lt {s a : ℝ} (hs : 0 < s) (hs' : s < 1) (ha : 0 < a) : 0 < boundaryQuadratic s a ↔ classicalThreshold s < a

theorem MetricCodes.Spherical.boundaryDegree_lt_longitudinal {s a : ℝ} (hs : 0 < s) (ha : 0 < a) (hquadratic : 0 < boundaryQuadratic s a) : boundaryDegree s a < a

theorem MetricCodes.Spherical.feasible_iff_boundary {s a b : ℝ} (hs : 0 < s) (hs' : s < 1) : Feasible s a b ↔ classicalThreshold s < a ∧ 0 < b ∧ b < boundaryDegree s a

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

The boundary 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.boundaryVariationalRate (s : ℝ) : ℝ

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

Equations

• MetricCodes.Spherical.boundaryVariationalRate s = sInf (MetricCodes.Spherical.boundaryRateSet s)

theorem MetricCodes.Spherical.boundaryRateSet_bddBelow {s : ℝ} (hs : 0 < s) (hs' : s < 1) : BddBelow (boundaryRateSet s)

theorem MetricCodes.Spherical.variationalRate_le_boundaryObjective {s a : ℝ} (hs : 0 < s) (hs' : s < 1) (hthreshold : classicalThreshold s < a) : variationalRate s ≤ sphericalEntropy a - sphericalEntropy (boundaryDegree s a)

theorem MetricCodes.Spherical.variationalRate_eq_boundaryVariationalRate {s : ℝ} (hs : 0 < s) (hs' : s < 1) : variationalRate s = boundaryVariationalRate s

theorem MetricCodes.Spherical.sphericalEntropy_upper_logb_add {a : ℝ} (ha : 0 < a) : sphericalEntropy a ≤ Real.logb 2 (1 + a) + 1 / Real.log 2

noncomputable def MetricCodes.Spherical.SidelnikovLocalization.sliceCost (s t : ℝ) : ℝ

The slice cost used in the spherical-code argument.

Equations

• MetricCodes.Spherical.SidelnikovLocalization.sliceCost s t = 1 / 2 * Real.logb 2 ((1 - t) / (1 - s))

theorem MetricCodes.Spherical.SidelnikovLocalization.sliceCost_nonneg {s t : ℝ} (hts : t ≤ s) (hs : s < 1) : 0 ≤ sliceCost s t

@[simp]

theorem MetricCodes.Spherical.SidelnikovLocalization.sliceCost_self {s : ℝ} (hs : s < 1) : sliceCost s s = 0

noncomputable def MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope (κ : ℝ → ℝ) (s : ℝ) : ℝ

The localized envelope used in the spherical-code argument.

Equations

• MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope κ s = sInf ((fun (t : ℝ) => κ t + MetricCodes.Spherical.SidelnikovLocalization.sliceCost s t) '' Set.Icc 0 s)

theorem MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope_bddBelow {κ : ℝ → ℝ} {s : ℝ} (hs : s < 1) (hκ : ∀ t ∈ Set.Icc 0 s, 0 ≤ κ t) : BddBelow ((fun (t : ℝ) => κ t + sliceCost s t) '' Set.Icc 0 s)

theorem MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope_le {κ : ℝ → ℝ} {s t : ℝ} (hs : s < 1) (ht : t ∈ Set.Icc 0 s) (hκ : ∀ x ∈ Set.Icc 0 s, 0 ≤ κ x) : localizedEnvelope κ s ≤ κ t + sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.interlacing_append {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {ε : ℝ} (hε : 0 < ε) (hεa : ε < a (Fin.last r)) : Interlacing (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ b ε)

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeNumerator_append_castSucc {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (ε : ℝ) (i : Fin (r + 1)) : lagrangeNumerator (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ b ε) i.castSucc = lagrangeNumerator a b i * (a i * (1 + a i) - ε * (1 + ε))

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator_append_castSucc {r : ℕ} (a : Fin (r + 1) → ℝ) (i : Fin (r + 1)) : lagrangeDenominator (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) i.castSucc = lagrangeDenominator a i * (a i * (1 + a i))

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeWeight_append_castSucc {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) (ε : ℝ) (i : Fin (r + 1)) : lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ b ε) i.castSucc = lagrangeWeight a b i * (1 - ε * (1 + ε) / (a i * (1 + a i)))

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_append {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) (ε : ℝ) : Gamma (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ b ε) = Gamma a b - ε * (1 + ε) * MetricCodes.Spherical.HigherHierarchy.appendSpectralLoss✝ a b

theorem MetricCodes.Spherical.HigherHierarchy.Phi_append {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (ε : ℝ) : Phi (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ a) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ b ε) = Phi a b - sphericalEntropy ε

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_nonneg {c u : ℝ} (hc : 0 ≤ c) (hu : 0 ≤ u) : 0 ≤ MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u

theorem MetricCodes.Spherical.HigherHierarchy.quadraticCoordinate_scaleCoordinate {c u : ℝ} (hc : 0 ≤ c) (hu : 0 ≤ u) : MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u * (1 + MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u) = c * (u * (1 + u))

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_one {u : ℝ} (hu : 0 ≤ u) : MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ 1 u = u

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_zero (c : ℝ) : MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c 0 = 0

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_strictMonoOn {c : ℝ} (hc : 0 < c) : StrictMonoOn (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c) (Set.Ici 0)

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_pos {c u : ℝ} (hc : 0 < c) (hu : 0 < u) : 0 < MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.scale {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {c : ℝ} (hc : 0 < c) : Interlacing (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ c a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ c b)

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeWeight_scale {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {c : ℝ} (hc : 0 < c) (i : Fin (r + 1)) : lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ c a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ c b) i = lagrangeWeight a b i

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

theorem MetricCodes.Spherical.HigherHierarchy.spectralAtom_strictMonoOn : StrictMonoOn spectralAtom (Set.Ici 0)

theorem MetricCodes.Spherical.HigherHierarchy.spectralAtom_scale_lt {c u : ℝ} (hc : 1 < c) (hu : 0 < u) : spectralAtom u < spectralAtom (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u)

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_scale_gt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) {c : ℝ} (hc : 1 < c) : Gamma a b < Gamma (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ c a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ c b)

theorem MetricCodes.Spherical.HigherHierarchy.spectralAtom_scale_sub_lower_bound {c u : ℝ} (hc : 1 ≤ c) (hc' : c ≤ 2) (hu : 0 ≤ u) : u * (1 + u) * (c - 1) / ((1 + 8 * (u * (1 + u))) * (1 + 4 * (u * (1 + u)))) ≤ spectralAtom (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u) - spectralAtom u

theorem MetricCodes.Spherical.HigherHierarchy.scalingGainCoefficient_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : 0 < MetricCodes.Spherical.HigherHierarchy.scalingGainCoefficient✝ a b

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_scale_sub_lower_bound {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {c : ℝ} (hc : 1 ≤ c) (hc' : c ≤ 2) : (c - 1) * MetricCodes.Spherical.HigherHierarchy.scalingGainCoefficient✝ a b ≤ Gamma (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ c a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ c b) - Gamma a b

theorem MetricCodes.Spherical.HigherHierarchy.appendSpectralLossUpper_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : 0 < MetricCodes.Spherical.HigherHierarchy.appendSpectralLossUpper✝ a b

theorem MetricCodes.Spherical.HigherHierarchy.append_scaled_spectralLoss_le {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) {c ε : ℝ} (hc : 0 < c) (hε : 0 ≤ ε) : MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c ε * (1 + MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c ε) * MetricCodes.Spherical.HigherHierarchy.appendSpectralLoss✝ (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ c a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ c b) ≤ ε * (1 + ε) * MetricCodes.Spherical.HigherHierarchy.appendSpectralLossUpper✝ a b

theorem MetricCodes.Spherical.HigherHierarchy.compensatedScalingSlope_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : 0 < MetricCodes.Spherical.HigherHierarchy.compensatedScalingSlope✝ a b

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_compensated_append_gt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) {ε : ℝ} (hε : 0 < ε) (hmoderate : MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε ≤ 2) : Gamma a b < Gamma (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) a)) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) b) (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) ε))

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor_zero {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b 0 = 1

theorem MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor_differentiableAt_zero {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : DifferentiableAt ℝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b) 0

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_compensated_differentiableAt_zero {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) {u : ℝ} (hu : 0 ≤ u) : DifferentiableAt ℝ (fun (ε : ℝ) => MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) u) 0

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.compensatedPhiPath_zero {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : MetricCodes.Spherical.HigherHierarchy.compensatedPhiPath✝ a b 0 = Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.compensatedPhiPath_differentiableAt_zero {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : DifferentiableAt ℝ (MetricCodes.Spherical.HigherHierarchy.compensatedPhiPath✝ a b) 0

theorem MetricCodes.Spherical.HigherHierarchy.eventually_sub_sphericalEntropy_lt_of_differentiable {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f 0) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), f ε - sphericalEntropy ε < f 0

theorem MetricCodes.Spherical.HigherHierarchy.le_scaleCoordinate_of_one_le {c u : ℝ} (hc : 1 ≤ c) (hu : 0 ≤ u) : u ≤ MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ c u

theorem MetricCodes.Spherical.HigherHierarchy.eventually_Phi_compensated_append_lt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), Phi (MetricCodes.Spherical.HigherHierarchy.appendAmbient✝ (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) a)) (MetricCodes.Spherical.HigherHierarchy.appendStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) b) (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (MetricCodes.Spherical.HigherHierarchy.compensatedScalingFactor✝ a b ε) ε)) < Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.exists_nextLevel_strict_refinement {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hlast : 0 < a (Fin.last r)) : ∃ (A : Fin (r + 2) → ℝ) (B : Fin (r + 1) → ℝ), Interlacing A B ∧ Gamma a b < Gamma A B ∧ Phi A B < Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.Phi_eq_sum_entropy_gaps {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : Phi a b = ∑ i : Fin r, (sphericalEntropy (a i.castSucc) - sphericalEntropy (b i)) + sphericalEntropy (a (Fin.last r))

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

noncomputable def MetricCodes.Spherical.HigherHierarchy.levelRate (r : ℕ) (s : ℝ) : ℝ

The level rate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.levelRate r s = sInf (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s)

theorem MetricCodes.Spherical.HigherHierarchy.levelRateSet_bddBelow (r : ℕ) (s : ℝ) : BddBelow (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s)

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

theorem MetricCodes.Spherical.HigherHierarchy.classical_le_levelRate_zero {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalEntropy (classicalThreshold s) ≤ levelRate 0 s

theorem MetricCodes.Spherical.HigherHierarchy.localizedEnvelope_lt_of_minimizer {κ κ' : ℝ → ℝ} {s t : ℝ} (hs : s < 1) (ht : t ∈ Set.Icc 0 s) (hκ' : ∀ x ∈ Set.Icc 0 s, 0 ≤ κ' x) (hmin : SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t) (hstrict : κ' t < κ t) : SidelnikovLocalization.localizedEnvelope κ' s < SidelnikovLocalization.localizedEnvelope κ s

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.openingAmbient_zero {r : ℕ} {a : Fin (r + 1) → ℝ} (hzero : a (Fin.last r) = 0) : MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a 0 0 = a

theorem MetricCodes.Spherical.HigherHierarchy.zero_ne_last_of_level_pos {r : ℕ} (hr : 0 < r) : 0 ≠ Fin.last r

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.const (η k : ℝ) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (x : ℝ) => k) fun (x : ℝ) => k

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.add {η : ℝ} {f g F G : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (h' : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η g G) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => f t + g t) fun (t : ℝ) => F t + G t

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.sub {η : ℝ} {f g F G : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (h' : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η g G) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => f t - g t) fun (t : ℝ) => F t - G t

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.mul {η : ℝ} {f g F G : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (h' : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η g G) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => f t * g t) fun (t : ℝ) => F t * G t

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.inv {η : ℝ} {f F : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (hne : F 0 ≠ 0) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => (f t)⁻¹) fun (t : ℝ) => (F t)⁻¹

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.div {η : ℝ} {f g F G : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (h' : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η g G) (hne : G 0 ≠ 0) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => f t / g t) fun (t : ℝ) => F t / G t

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.sqrt {η : ℝ} {f F : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (hne : F 0 ≠ 0) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => √(f t)) fun (t : ℝ) => √(F t)

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.finset_sum {ι : Type u_1} {η : ℝ} (s : Finset ι) {f F : ι → ℝ → ℝ} (h : ∀ i ∈ s, MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (f i) (F i)) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => ∑ i ∈ s, f i t) fun (t : ℝ) => ∑ i ∈ s, F i t

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.finset_prod {ι : Type u_1} {η : ℝ} (s : Finset ι) {f F : ι → ℝ → ℝ} (h : ∀ i ∈ s, MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (f i) (F i)) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => ∏ i ∈ s, f i t) fun (t : ℝ) => ∏ i ∈ s, F i t

theorem MetricCodes.Spherical.HigherHierarchy.openingAmbient_scaledDerivative {r : ℕ} (a : Fin (r + 1) → ℝ) (η : ℝ) (i : Fin (r + 1)) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2) i) fun (t : ℝ) => MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a t (t ^ 2) i

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.quadraticCoordinate {η : ℝ} {f F : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => f t * (1 + f t)) fun (t : ℝ) => F t * (1 + F t)

theorem MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative.spectralAtom {η : ℝ} {f F : ℝ → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η f F) (hpositive : 0 < F 0) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => HigherHierarchy.spectralAtom (f t)) fun (t : ℝ) => HigherHierarchy.spectralAtom (F t)

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeWeight_opening_scaledDerivative {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) (i : Fin (r + 1)) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (fun (t : ℝ) => lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b i) fun (t : ℝ) => lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a t (t ^ 2)) b i

theorem MetricCodes.Spherical.HigherHierarchy.openingRegularGamma_scaledDerivative {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) : MetricCodes.Spherical.HigherHierarchy.ScaledOpeningDerivative✝ η (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b η) (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b 1)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_spectralAtom_sq_div : Filter.Tendsto (fun (t : ℝ) => spectralAtom (t ^ 2) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_sphericalEntropy_sq_div : Filter.Tendsto (fun (t : ℝ) => sphericalEntropy (t ^ 2) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_opening_entropy_slope {a η : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (t : ℝ) => (sphericalEntropy (a - η * t) - sphericalEntropy a + sphericalEntropy (t ^ 2)) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(η * Real.logb 2 ((1 + a) / a))))

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_opening_eq_regular_add {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (η t : ℝ) : Gamma (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b = MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b η t + lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b (Fin.last r) * spectralAtom (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.openingRegularGamma_zero {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (hzero : a (Fin.last r) = 0) (η : ℝ) : MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b η 0 = Gamma a b

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_opening_terminalWeight {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) : Filter.Tendsto (fun (t : ℝ) => lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b (Fin.last r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (lagrangeWeight a b (Fin.last r)))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_openingRegularGamma_slope {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) : Filter.Tendsto (fun (t : ℝ) => (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b η t - Gamma a b) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (η * deriv (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b 1) 0))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Gamma_opening_slope {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) : Filter.Tendsto (fun (t : ℝ) => (Gamma (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b - Gamma a b) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (η * deriv (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b 1) 0 + lagrangeWeight a b (Fin.last r)))

theorem MetricCodes.Spherical.HigherHierarchy.sum_sphericalEntropy_update {n : ℕ} (a : Fin n → ℝ) (i : Fin n) (x : ℝ) : ∑ j : Fin n, sphericalEntropy (Function.update a i x j) = ∑ j : Fin n, sphericalEntropy (a j) - sphericalEntropy (a i) + sphericalEntropy x

theorem MetricCodes.Spherical.HigherHierarchy.Phi_opening_eq {r : ℕ} (hr : 0 < r) {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (hzero : a (Fin.last r) = 0) (η t : ℝ) : Phi (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b - Phi a b = sphericalEntropy (a 0 - η * t) - sphericalEntropy (a 0) + sphericalEntropy (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_Phi_opening_lt {r : ℕ} (hr : 0 < r) {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) {η : ℝ} (hη : 0 < η) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), Phi (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b < Phi a b

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

theorem MetricCodes.Spherical.HigherHierarchy.opening_spectralSlope_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : 0 < MetricCodes.Spherical.HigherHierarchy.openingContractionSpeed✝ a b * deriv (MetricCodes.Spherical.HigherHierarchy.openingRegularGamma✝ a b 1) 0 + lagrangeWeight a b (Fin.last r)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_Gamma_opening_gt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), Gamma a b < Gamma (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (MetricCodes.Spherical.HigherHierarchy.openingContractionSpeed✝ a b * t) (t ^ 2)) b

theorem MetricCodes.Spherical.HigherHierarchy.eventually_opening_interlacing {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) (η : ℝ) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), Interlacing (MetricCodes.Spherical.HigherHierarchy.openingAmbient✝ a (η * t) (t ^ 2)) b

theorem MetricCodes.Spherical.HigherHierarchy.exists_sameLevel_opening_strict_refinement {r : ℕ} (hr : 0 < r) {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hzero : a (Fin.last r) = 0) : ∃ (A : Fin (r + 1) → ℝ), 0 < A (Fin.last r) ∧ Interlacing A b ∧ Gamma a b < Gamma A b ∧ Phi A b < Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.exists_nextLevel_feasible_lt {r : ℕ} {s : ℝ} (hs : 0 < s) {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (hgap : s < 2 * Gamma a b) : ∃ (A : Fin (r + 2) → ℝ) (B : Fin (r + 1) → ℝ), Interlacing A B ∧ s < 2 * Gamma A B ∧ Phi A B < Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_nonneg_of_nonempty {r : ℕ} {s : ℝ} (h : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s).Nonempty) : 0 ≤ levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_succ_le_of_feasible {r : ℕ} {s : ℝ} (hs : 0 < s) (h : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s).Nonempty) : levelRate (r + 1) s ≤ levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.levelRateSet_zero_nonempty_of_interior {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ 0 s).Nonempty

theorem MetricCodes.Spherical.HigherHierarchy.levelRateSet_nonempty_of_interior (r : ℕ) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s).Nonempty

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_succ_le {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : levelRate (r + 1) s ≤ levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_le_levelRate_zero {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : levelRate r s ≤ levelRate 0 s

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_mono {r : ℕ} {s t : ℝ} (hst : s ≤ t) (ht : 0 < t) (ht' : t < 1) : levelRate r s ≤ levelRate r t

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_nonneg_all (r : ℕ) (s : ℝ) : 0 ≤ levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_nonnegOn_Icc (r : ℕ) (s t : ℝ) : t ∈ Set.Icc 0 s → 0 ≤ levelRate r t

theorem MetricCodes.Spherical.HigherHierarchy.exists_localized_minimizer_of_lowerSemicontinuous {κ : ℝ → ℝ} {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) (hκ : ∀ t ∈ Set.Icc 0 s, 0 ≤ κ t) (hlsc : LowerSemicontinuousOn (fun (t : ℝ) => κ t + SidelnikovLocalization.sliceCost s t) (Set.Icc 0 s)) : ∃ t ∈ Set.Icc 0 s, SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_minimizer_of_lowerSemicontinuous {κ : ℝ → ℝ} {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) (hκ : ∀ t ∈ Set.Icc 0 s, 0 ≤ κ t) (hlsc : LowerSemicontinuousOn (fun (t : ℝ) => κ t + SidelnikovLocalization.sliceCost s t) (Set.Icc 0 s)) (hzero : ∃ u ∈ Set.Icc 0 s, κ u + SidelnikovLocalization.sliceCost s u < κ 0 + SidelnikovLocalization.sliceCost s 0) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.sliceCost_sub_zero {s t : ℝ} (hs : s < 1) (ht : t < 1) : SidelnikovLocalization.sliceCost s t - SidelnikovLocalization.sliceCost s 0 = 1 / 2 * Real.logb 2 (1 - t)

theorem MetricCodes.Spherical.HigherHierarchy.sliceCost_sub_zero_le_neg_linear {s t : ℝ} (hs : s < 1) (ht : t < 1) : SidelnikovLocalization.sliceCost s t - SidelnikovLocalization.sliceCost s 0 ≤ -t / (2 * Real.log 2)

theorem MetricCodes.Spherical.HigherHierarchy.sliceCost_continuousOn {s : ℝ} (hs : s < 1) : ContinuousOn (SidelnikovLocalization.sliceCost s) (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_le_squared_entropy_of_spectral {t : ℝ} (ht : 0 < t) (hspectral : t < 2 * spectralAtom (t ^ 2)) : levelRate 0 t ≤ sphericalEntropy (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_squared_spectralCertificate : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), t < 2 * spectralAtom (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_levelRate_zero_le_squared_entropy : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), levelRate 0 t ≤ sphericalEntropy (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.exists_sliceCost_endpoint_improvement_of_smallEntropy {κ : ℝ → ℝ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hzero : κ 0 = 0) (hsmall : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), κ t ≤ sphericalEntropy (t ^ 2)) : ∃ u ∈ Set.Icc 0 s, κ u + SidelnikovLocalization.sliceCost s u < κ 0 + SidelnikovLocalization.sliceCost s 0

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_minimizer_of_lsc_and_smallEntropy {κ : ℝ → ℝ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hκ : ∀ t ∈ Set.Icc 0 s, 0 ≤ κ t) (hzero : κ 0 = 0) (hsmall : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), κ t ≤ sphericalEntropy (t ^ 2)) (hlsc : LowerSemicontinuousOn κ (Set.Icc 0 s)) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_levelRate_minimizer_of_lsc_and_zero {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hκ : ∀ t ∈ Set.Icc 0 s, 0 ≤ levelRate r t) (hzero : levelRate r 0 = 0) (hupper : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), levelRate r t ≤ levelRate 0 t) (hlsc : LowerSemicontinuousOn (levelRate r) (Set.Icc 0 s)) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope (levelRate r) s = levelRate r t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_at_zero (r : ℕ) : levelRate r 0 = 0

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_levelRate_minimizer_of_lsc {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlsc : LowerSemicontinuousOn (levelRate r) (Set.Icc 0 s)) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope (levelRate r) s = levelRate r t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.logb_one_add_le_sphericalEntropy {u : ℝ} (hu : 0 ≤ u) : Real.logb 2 (1 + u) ≤ sphericalEntropy u

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

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.terminal_entropy_le_Phi {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : sphericalEntropy (a (Fin.last r)) ≤ Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.entropy_gap_le_Phi {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin r) : sphericalEntropy (a i.castSucc) - sphericalEntropy (b i) ≤ Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.degree_le_rpow_sub_one_of_sphericalEntropy_le {u C : ℝ} (hu : 0 ≤ u) (hC : sphericalEntropy u ≤ C) : u ≤ 2 ^ C - 1

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.terminal_degree_le_rpow_sub_one_of_Phi_le {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {C : ℝ} (hC : Phi a b ≤ C) : a (Fin.last r) ≤ 2 ^ C - 1

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.shifted_degree_ratio_le_rpow_of_entropy_gap_le {a b C : ℝ} (hb : 0 < b) (hba : b ≤ a) (hC : sphericalEntropy a - sphericalEntropy b ≤ C) : (1 + a) / (1 + b) ≤ 2 ^ (C + 1 / Real.log 2)

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.degree_ratio_lower_bound_of_entropy_gap_le {a b C : ℝ} (hb : 1 ≤ b) (hba : b ≤ a) (hC : sphericalEntropy a - sphericalEntropy b ≤ C) : (2 * 2 ^ (C + 1 / Real.log 2))⁻¹ ≤ b / a

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_sphericalEntropy_sub_logb_one_add : Filter.Tendsto (fun (a : ℝ) => sphericalEntropy a - Real.logb 2 (1 + a)) Filter.atTop (nhds (1 / Real.log 2))

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_sphericalEntropy_sub_of_ratio {f : ℝ → ℝ} {c : ℝ} (hc : 0 < c) (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (a : ℝ) => f a / a) Filter.atTop (nhds c)) : Filter.Tendsto (fun (a : ℝ) => sphericalEntropy a - sphericalEntropy (f a)) Filter.atTop (nhds (-Real.logb 2 c))

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.sqrt_degree_mul_one_add_eq {a : ℝ} (ha : 0 < a) : √(a * (1 + a)) = a * √(1 + a⁻¹)

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.boundaryQuadratic_eq_sq_mul_normalized {s a : ℝ} (ha : 0 < a) : boundaryQuadratic s a = a ^ 2 * MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.normalizedBoundaryQuadratic✝ s a⁻¹

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.boundaryDegree_div_eq_normalized {s a : ℝ} (ha : 0 < a) : boundaryDegree s a / a = MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.normalizedBoundaryDegree✝ s a⁻¹

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_boundaryDegree_div {s : ℝ} : Filter.Tendsto (fun (a : ℝ) => boundaryDegree s a / a) Filter.atTop (nhds √(1 - s))

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_boundaryDegree_atTop {s : ℝ} (hs : s < 1) : Filter.Tendsto (boundaryDegree s) Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_entropy_sub_boundaryDegree {s : ℝ} (hs' : s < 1) : Filter.Tendsto (fun (a : ℝ) => sphericalEntropy a - sphericalEntropy (boundaryDegree s a)) Filter.atTop (nhds (-(1 / 2) * Real.logb 2 (1 - s)))

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_mem_Ioc {u : ℝ} (hu : 0 ≤ u) : MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ u ∈ Set.Ioc 0 1

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_mem_Icc {u : ℝ} (hu : 0 ≤ u) : MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ u ∈ Set.Icc 0 1

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_inv_sub_one (u : ℝ) : (MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ u)⁻¹ - 1 = u

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_of_compactifiedHierarchyCoordinate_pos {f : ℕ → ℝ} {x : ℝ} (hx : 0 < x) (h : Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (f k)) Filter.atTop (nhds x)) : Filter.Tendsto f Filter.atTop (nhds (x⁻¹ - 1))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_atTop_of_compactifiedHierarchyCoordinate_zero {f : ℕ → ℝ} (hf : ∀ (k : ℕ), 0 ≤ f k) (h : Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (f k)) Filter.atTop (nhds 0)) : Filter.Tendsto f Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_limit_pos_of_bddAbove {f : ℕ → ℝ} {x C : ℝ} (hf : ∀ (k : ℕ), 0 ≤ f k) (hC : ∀ (k : ℕ), f k ≤ C) (h : Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (f k)) Filter.atTop (nhds x)) : 0 < x

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_antitone {u v : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (h : u ≤ v) : MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ v ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ u

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_recovered_nonneg {x : ℝ} (hx : 0 < x) (hx' : x ≤ 1) : 0 ≤ x⁻¹ - 1

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate_recovered_antitone {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxy : x ≤ y) : y⁻¹ - 1 ≤ x⁻¹ - 1

theorem MetricCodes.Spherical.HigherHierarchy.exists_levelRate_minimizing_sequence {r : ℕ} {s : ℝ} (hne : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r s).Nonempty) : ∃ (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ), (∀ (k : ℕ), Interlacing (a k) (b k) ∧ s < 2 * Gamma (a k) (b k)) ∧ (Antitone fun (k : ℕ) => Phi (a k) (b k)) ∧ Filter.Tendsto (fun (k : ℕ) => Phi (a k) (b k)) Filter.atTop (nhds (levelRate r s))

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_minimizing_sequence_bddAbove {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} (hanti : Antitone fun (k : ℕ) => Phi (a k) (b k)) (k : ℕ) : Phi (a k) (b k) ≤ Phi (a 0) (b 0)

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyTuple_mem_cube {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyTuple✝ a b ∈ MetricCodes.Spherical.HigherHierarchy.hierarchyCompactCube✝ r

theorem MetricCodes.Spherical.HigherHierarchy.isCompact_hierarchyCompactCube (r : ℕ) : IsCompact (MetricCodes.Spherical.HigherHierarchy.hierarchyCompactCube✝ r)

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactifiedHierarchyTuple_subsequence {r : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) (h : ∀ (k : ℕ), Interlacing (a k) (b k)) : ∃ (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (φ : ℕ → ℕ), StrictMono φ ∧ (∀ (i : Fin (r + 1)), A i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), B i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin (r + 1)), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ k) i)) Filter.atTop (nhds (A i))) ∧ ∀ (i : Fin r), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ k) i)) Filter.atTop (nhds (B i))

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyTuple_limit_weak_interlacing {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} {φ : ℕ → ℕ} (h : ∀ (k : ℕ), Interlacing (a k) (b k)) (hA : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ k) i)) Filter.atTop (nhds (A i))) (hB : ∀ (i : Fin r), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ k) i)) Filter.atTop (nhds (B i))) (i : Fin r) : A i.castSucc ≤ B i ∧ B i ≤ A i.succ

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyTuple_recovered_weak_interlacing {r : ℕ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} (hA : ∀ (i : Fin (r + 1)), A i ∈ Set.Ioc 0 1) (hB : ∀ (i : Fin r), B i ∈ Set.Ioc 0 1) (hinter : ∀ (i : Fin r), A i.castSucc ≤ B i ∧ B i ≤ A i.succ) : 0 ≤ (A (Fin.last r))⁻¹ - 1 ∧ ∀ (i : Fin r), (B i)⁻¹ - 1 ≤ (A i.castSucc)⁻¹ - 1 ∧ (A i.succ)⁻¹ - 1 ≤ (B i)⁻¹ - 1

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyTuple_terminal_limit_pos {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {φ : ℕ → ℕ} {C : ℝ} (h : ∀ (k : ℕ), Interlacing (a k) (b k)) (hbound : ∀ (k : ℕ), Phi (a k) (b k) ≤ C) (hA : Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ k) (Fin.last r))) Filter.atTop (nhds (A (Fin.last r)))) : 0 < A (Fin.last r)

theorem MetricCodes.Spherical.HigherHierarchy.exists_bounded_hierarchy_entropy_subsequence {r : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) {C : ℝ} (h : ∀ (k : ℕ), Interlacing (a k) (b k)) (hbound : ∀ (k : ℕ), Phi (a k) (b k) ≤ C) : ∃ (L : ℝ) (φ : ℕ → ℕ), StrictMono φ ∧ L ∈ Set.Icc 0 C ∧ Filter.Tendsto (fun (k : ℕ) => Phi (a (φ k)) (b (φ k))) Filter.atTop (nhds L)

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactified_bounded_hierarchy_subsequence {r : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) {C : ℝ} (h : ∀ (k : ℕ), Interlacing (a k) (b k)) (hbound : ∀ (k : ℕ), Phi (a k) (b k) ≤ C) : ∃ (L : ℝ) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (φ : ℕ → ℕ), StrictMono φ ∧ L ∈ Set.Icc 0 C ∧ (∀ (i : Fin (r + 1)), A i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), B i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin (r + 1)), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ k) i)) Filter.atTop (nhds (A i))) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (k : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ k) i)) Filter.atTop (nhds (B i))) ∧ (∀ (i : Fin r), A i.castSucc ≤ B i ∧ B i ≤ A i.succ) ∧ 0 < A (Fin.last r) ∧ Filter.Tendsto (fun (k : ℕ) => Phi (a (φ k)) (b (φ k))) Filter.atTop (nhds L)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_lowerSemicontinuousOn_of_compactifiedCertificateClosure {r : ℕ} {s : ℝ} (_hs : 0 ≤ s) (hs' : s < 1) (hclosure : MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r) : LowerSemicontinuousOn (levelRate r) (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.interlacing_prepend {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {u v : ℝ} (huv : v < u) (hva : a 0 < v) : Interlacing (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b)

theorem MetricCodes.Spherical.HigherHierarchy.Phi_prepend {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (u v : ℝ) : Phi (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) = Phi a b + (sphericalEntropy u - sphericalEntropy v)

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeNumerator_prepend_succ {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (u v : ℝ) (i : Fin (r + 1)) : lagrangeNumerator (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) i.succ = (a i * (1 + a i) - v * (1 + v)) * lagrangeNumerator a b i

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeDenominator_prepend_succ {r : ℕ} (a : Fin (r + 1) → ℝ) (u : ℝ) (i : Fin (r + 1)) : lagrangeDenominator (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) i.succ = (a i * (1 + a i) - u * (1 + u)) * lagrangeDenominator a i

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeWeight_prepend_succ {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (u v : ℝ) (i : Fin (r + 1)) (hne : a i * (1 + a i) - u * (1 + u) ≠ 0) : lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) i.succ = lagrangeWeight a b i * ((a i * (1 + a i) - v * (1 + v)) / (a i * (1 + a i) - u * (1 + u)))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_scaleCoordinate_sq_div_atTop {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u / u) Filter.atTop (nhds c)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_scaleCoordinate_sq_atTop {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.scaleCoordinate_sq_lt_self {c u : ℝ} (hc : 0 < c) (hc' : c < 1) (hu : 0 < u) : MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u < u

theorem MetricCodes.Spherical.HigherHierarchy.eventually_interlacing_prepend_scale {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {c : ℝ} (hc : 0 < c) (hc' : c < 1) : ∀ᶠ (u : ℝ) in Filter.atTop, Interlacing (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_entropy_prepend_scale {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => sphericalEntropy u - sphericalEntropy (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u)) Filter.atTop (nhds (-Real.logb 2 c))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Phi_prepend_scale {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => Phi (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b)) Filter.atTop (nhds (Phi a b - Real.logb 2 c))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_spectralAtom_atTop_half : Filter.Tendsto spectralAtom Filter.atTop (nhds (1 / 2))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_retainedQuadraticResidueFactor_atTop (z c : ℝ) : Filter.Tendsto (fun (u : ℝ) => (z * (1 + z) - c ^ 2 * (u * (1 + u))) / (z * (1 + z) - u * (1 + u))) Filter.atTop (nhds (c ^ 2))

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_prepend_eq_spectralAtom_add_retained {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (u v : ℝ) (h : Interlacing (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b)) : Gamma (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) = spectralAtom u + ∑ i : Fin (r + 1), lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) i.succ * (spectralAtom (a i) - spectralAtom u)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_lagrangeWeight_prepend_scale_succ {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (c : ℝ) (i : Fin (r + 1)) : Filter.Tendsto (fun (u : ℝ) => lagrangeWeight (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b) i.succ) Filter.atTop (nhds (c ^ 2 * lagrangeWeight a b i))

theorem MetricCodes.Spherical.HigherHierarchy.prepend_spectral_limit_algebra {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (c : ℝ) : 1 / 2 + ∑ i : Fin (r + 1), c ^ 2 * lagrangeWeight a b i * (spectralAtom (a i) - 1 / 2) = (1 - c ^ 2) / 2 + c ^ 2 * Gamma a b

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Gamma_prepend_scale {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {c : ℝ} (hc : 0 < c) (hc' : c < 1) : Filter.Tendsto (fun (u : ℝ) => Gamma (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b)) Filter.atTop (nhds ((1 - c ^ 2) / 2 + c ^ 2 * Gamma a b))

theorem MetricCodes.Spherical.HigherHierarchy.rateSet_subset_hierarchyRateSet (s : ℝ) : rateSet s ⊆ hierarchyRateSet s

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyRateSet_nonempty_of_interior {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (hierarchyRateSet s).Nonempty

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_nonneg {s : ℝ} (hs : 0 < s) (hs' : s < 1) : 0 ≤ hierarchyVariationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.exists_nextLevel_compactified_certificate_lt_of_spectral_limit {r : ℕ} {s c R : ℝ} (hc : 0 < c) (hc' : c < 1) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (hscaled : s < 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hR : Phi a b - Real.logb 2 c < R) (hGamma : Filter.Tendsto (fun (u : ℝ) => Gamma (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b)) Filter.atTop (nhds ((1 - c ^ 2) / 2 + c ^ 2 * Gamma a b))) : ∃ (A : Fin (r + 2) → ℝ) (B : Fin (r + 1) → ℝ), Interlacing A B ∧ s < 2 * Gamma A B ∧ Phi A B < R

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_compactified_certificate_of_spectral_limit {r : ℕ} {s c : ℝ} (hc : 0 < c) (hc' : c < 1) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (hscaled : s < 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hGamma : Filter.Tendsto (fun (u : ℝ) => Gamma (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ (MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ (c ^ 2) u) b)) Filter.atTop (nhds ((1 - c ^ 2) / 2 + c ^ 2 * Gamma a b))) : hierarchyVariationalRate s ≤ Phi a b - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.exists_nextLevel_compactified_certificate_lt {r : ℕ} {s c R : ℝ} (hc : 0 < c) (hc' : c < 1) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (hscaled : s < 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hR : Phi a b - Real.logb 2 c < R) : ∃ (A : Fin (r + 2) → ℝ) (B : Fin (r + 1) → ℝ), Interlacing A B ∧ s < 2 * Gamma A B ∧ Phi A B < R

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_succ_le_compactified_certificate {r : ℕ} {s c : ℝ} (hc : 0 < c) (hc' : c < 1) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (hscaled : s < 1 - c ^ 2 * (1 - 2 * Gamma a b)) : levelRate (r + 1) s ≤ Phi a b - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_antitone_level {s : ℝ} (hs : 0 < s) (hs' : s < 1) {j k : ℕ} (hjk : j ≤ k) : levelRate k s ≤ levelRate j s

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_le_compactified_datum {k j : ℕ} {s c : ℝ} (hs : 0 < s) (hs' : s < 1) (hc : 0 < c) (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ) (h : Interlacing a b) (hscaled : s < 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hlevels : c = 1 ∧ j ≤ k ∨ c < 1 ∧ j + 1 ≤ k) : levelRate k s ≤ Phi a b - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.continuous_scaleCoordinate_factor (u : ℝ) : Continuous fun (t : ℝ) => MetricCodes.Spherical.HigherHierarchy.scaleCoordinate✝ t u

theorem MetricCodes.Spherical.HigherHierarchy.continuous_Phi_common_scale {j : ℕ} (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ) : Continuous fun (t : ℝ) => Phi (MetricCodes.Spherical.HigherHierarchy.scaleAmbient✝ t a) (MetricCodes.Spherical.HigherHierarchy.scaleStabilizer✝ t b)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_le_of_non_strict_spectral {j : ℕ} {s : ℝ} (hs : 0 < s) (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ) (h : Interlacing a b) (hboundary : s ≤ 2 * Gamma a b) : levelRate j s ≤ Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_le_compactified_boundary_datum {r j : ℕ} {s c : ℝ} (hs : 0 < s) (hs' : s < 1) (hc : 0 < c) (hc' : c ≤ 1) (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ) (h : Interlacing a b) (hscaled : s ≤ 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hlevels : c = 1 ∧ j ≤ r ∨ c < 1 ∧ j + 1 ≤ r) : levelRate r s ≤ Phi a b - Real.logb 2 c

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

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPhase_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : 0 ≤ stieltjesPhase a b t

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPhaseProduct_pos {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : 0 < stieltjesPhaseProduct a b t

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPhaseProduct_le_one {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) {t : ℝ} (ht : 0 < t) : stieltjesPhaseProduct a b t ≤ 1

theorem MetricCodes.Spherical.HigherHierarchy.WeakInterlacing.antitone_ambient {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) : Antitone a

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

theorem MetricCodes.Spherical.HigherHierarchy.WeakInterlacing.tail {r : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ (Fin.tail a) (Fin.tail b)

theorem MetricCodes.Spherical.HigherHierarchy.WeakInterlacing.drop_second {r : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) (hcollision : b 0 = a 1) : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ (Fin.cons (a 0) (Fin.tail (Fin.tail a))) (Fin.tail b)

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio_prepend {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (u v t : ℝ) : MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (MetricCodes.Spherical.HigherHierarchy.prependAmbient✝ u a) (MetricCodes.Spherical.HigherHierarchy.prependStabilizer✝ v b) t = (t + v * (1 + v)) / (t + u * (1 + u)) * MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a b t

theorem MetricCodes.Spherical.HigherHierarchy.Phi_tail_of_head_collision {r : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hcollision : a 0 = b 0) : Phi a b = Phi (Fin.tail a) (Fin.tail b)

theorem MetricCodes.Spherical.HigherHierarchy.Phi_drop_second_of_collision {r : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hcollision : b 0 = a 1) : Phi a b = Phi (Fin.cons (a 0) (Fin.tail (Fin.tail a))) (Fin.tail b)

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio_tail_of_head_collision {r : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) (hcollision : a 0 = b 0) {t : ℝ} (ht : 0 < t) : MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a b t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (Fin.tail a) (Fin.tail b) t

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio_drop_second_of_collision {r : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) (hcollision : b 0 = a 1) {t : ℝ} (ht : 0 < t) : MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a b t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (Fin.cons (a 0) (Fin.tail (Fin.tail a))) (Fin.tail b) t

theorem MetricCodes.Spherical.HigherHierarchy.exists_strict_residual_of_weak_interlacing {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ a b) : ∃ (j : ℕ) (A : Fin (j + 1) → ℝ) (B : Fin j → ℝ), j ≤ r ∧ Interlacing A B ∧ Phi A B = Phi a b ∧ ∀ (t : ℝ), 0 < t → (∏ i : Fin r, (t + b i * (1 + b i))) / ∏ i : Fin (r + 1), (t + a i * (1 + a i)) = (∏ i : Fin j, (t + B i * (1 + B i))) / ∏ i : Fin (j + 1), (t + A i * (1 + A i))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_shifted_degree_ratio_of_tendsto_ratio {u v : ℕ → ℝ} {d : ℝ} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => v n / u n) Filter.atTop (nhds d)) : Filter.Tendsto (fun (n : ℕ) => (1 + v n) / (1 + u n)) Filter.atTop (nhds d)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_sphericalEntropy_sub_of_sequence_ratio {u v : ℕ → ℝ} {d : ℝ} (hd : 0 < d) (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => v n / u n) Filter.atTop (nhds d)) : Filter.Tendsto (fun (n : ℕ) => sphericalEntropy (u n) - sphericalEntropy (v n)) Filter.atTop (nhds (-Real.logb 2 d))

theorem MetricCodes.Spherical.HigherHierarchy.paired_stabilizer_tendsto_atTop_of_ambient {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {φ : ℕ → ℕ} {C : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (i : Fin r) (ha : Filter.Tendsto (fun (n : ℕ) => a (φ n) i.castSucc) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => b (φ n) i) Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.paired_infinity_iff {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} {φ : ℕ → ℕ} {C : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (hA : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) (hB : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) (hAnonneg : ∀ (i : Fin (r + 1)), 0 ≤ A i) (i : Fin r) : A i.castSucc = 0 ↔ B i = 0

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedAmbient_monotone_of_weak_interlacing {r : ℕ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} (hinter : ∀ (i : Fin r), A i.castSucc ≤ B i ∧ B i ≤ A i.succ) : Monotone A

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_compactified_suffix {r : ℕ} (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (hA : ∀ (i : Fin (r + 1)), A i ∈ Set.Icc 0 1) (hB : ∀ (i : Fin r), B i ∈ Set.Icc 0 1) (hinter : ∀ (i : Fin r), A i.castSucc ≤ B i ∧ B i ≤ A i.succ) (hpaired : ∀ (i : Fin r), A i.castSucc = 0 ↔ B i = 0) (hlast : 0 < A (Fin.last r)) : ∃ (k : ℕ) (j : ℕ) (hkj : k + j = r), (∀ (i : Fin r), ↑i < k → A i.castSucc = 0 ∧ B i = 0) ∧ (∀ (i : Fin (j + 1)), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i ∈ Set.Ioc 0 1) ∧ (∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∈ Set.Ioc 0 1) ∧ ∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.castSucc ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∧ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.succ

theorem MetricCodes.Spherical.HigherHierarchy.compactified_finite_suffix_weak_interlacing {r k j : ℕ} (hkj : k + j = r) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (hA : ∀ (i : Fin (j + 1)), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i ∈ Set.Ioc 0 1) (hB : ∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∈ Set.Ioc 0 1) (hinter : ∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.castSucc ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∧ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.succ) : MetricCodes.Spherical.HigherHierarchy.WeakInterlacing✝ (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_quadraticCoordinate_ratio_of_tendsto_degree_ratio {u v : ℕ → ℝ} {d : ℝ} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => v n / u n) Filter.atTop (nhds d)) : Filter.Tendsto (fun (n : ℕ) => v n * (1 + v n) / (u n * (1 + u n))) Filter.atTop (nhds (d ^ 2))

theorem MetricCodes.Spherical.HigherHierarchy.interlacing_paired_degree_ratio_mem_Icc {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) (i : Fin r) : b i / a i.castSucc ∈ Set.Icc 0 1

theorem MetricCodes.Spherical.HigherHierarchy.paired_ratio_limit_pos_of_ambient_tendsto_atTop {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {φ : ℕ → ℕ} {C d : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (i : Fin r) (ha : Filter.Tendsto (fun (n : ℕ) => a (φ n) i.castSucc) Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds d)) : 0 < d

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactified_paired_ratio_subsequence {r : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) {C : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) : ∃ (d : Fin r → ℝ) (φ : ℕ → ℕ), StrictMono φ ∧ (∀ (i : Fin r), d i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => a (φ n) i.castSucc) Filter.atTop Filter.atTop → 0 < d i) ∧ ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => a (φ n) i.castSucc) Filter.atTop Filter.atTop → Filter.Tendsto (fun (n : ℕ) => b (φ n) i * (1 + b (φ n) i) / (a (φ n) i.castSucc * (1 + a (φ n) i.castSucc))) Filter.atTop (nhds (d i ^ 2))

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactified_residual_of_closure_sequence {r : ℕ} {s R : ℝ} (u : ℕ → ℝ) (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) (hu : Filter.Tendsto u Filter.atTop (nhds s)) (hinter : ∀ (n : ℕ), Interlacing (a n) (b n)) (hgap : ∀ (n : ℕ), u n < 2 * Gamma (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ R + 1 / (↑n + 1)) : ∃ (L : ℝ) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (d : Fin r → ℝ) (φ : ℕ → ℕ) (k : ℕ) (j : ℕ) (hkj : k + j = r) (q : ℕ) (a₀ : Fin (q + 1) → ℝ) (b₀ : Fin q → ℝ) (c : ℝ), StrictMono φ ∧ 0 ≤ L ∧ L ≤ R ∧ (∀ (i : Fin (r + 1)), A i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), B i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) ∧ Filter.Tendsto (fun (n : ℕ) => u (φ n)) Filter.atTop (nhds s) ∧ (∀ (n : ℕ), u (φ n) < 2 * Gamma (a (φ n)) (b (φ n))) ∧ Filter.Tendsto (fun (n : ℕ) => Phi (a (φ n)) (b (φ n))) Filter.atTop (nhds L) ∧ (∀ (i : Fin r), d i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) ∧ (∀ (i : Fin r), A i.castSucc = 0 ↔ B i = 0) ∧ (∀ (i : Fin r), A i.castSucc = 0 → 0 < d i ∧ Filter.Tendsto (fun (n : ℕ) => b (φ n) i * (1 + b (φ n) i) / (a (φ n) i.castSucc * (1 + a (φ n) i.castSucc))) Filter.atTop (nhds (d i ^ 2))) ∧ q ≤ j ∧ Interlacing a₀ b₀ ∧ (∀ (i : Fin r), ↑i < k → A i.castSucc = 0 ∧ B i = 0) ∧ (∀ (i : Fin r), A i.castSucc = 0 ↔ ↑i < k) ∧ (∀ (i : Fin (j + 1)), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i ∈ Set.Ioc 0 1) ∧ (∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∈ Set.Ioc 0 1) ∧ (∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.castSucc ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∧ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.succ) ∧ (Phi a₀ b₀ = Phi (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) ∧ (∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) (fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a₀ b₀ t) ∧ c = ∏ i : Fin r with ↑i < k, d i ∧ 0 < c ∧ c ≤ 1 ∧ (c < 1 → q < r)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_entropy_gap_of_compactified_paired_ratio {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B d : Fin r → ℝ} {φ : ℕ → ℕ} {C : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (hA : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) (hB : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) (hAnonneg : ∀ (i : Fin (r + 1)), 0 ≤ A i) (hBnonneg : ∀ (i : Fin r), 0 ≤ B i) (hd : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) (i : Fin r) : Filter.Tendsto (fun (n : ℕ) => sphericalEntropy (a (φ n) i.castSucc) - sphericalEntropy (b (φ n) i)) Filter.atTop (nhds (if A i.castSucc = 0 then -Real.logb 2 (d i) else sphericalEntropy ((A i.castSucc)⁻¹ - 1) - sphericalEntropy ((B i)⁻¹ - 1)))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Phi_of_compactified_paired_ratios {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B d : Fin r → ℝ} {φ : ℕ → ℕ} {C : ℝ} (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (hA : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) (hB : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) (hAnonneg : ∀ (i : Fin (r + 1)), 0 ≤ A i) (hBnonneg : ∀ (i : Fin r), 0 ≤ B i) (hlast : 0 < A (Fin.last r)) (hd : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) : Filter.Tendsto (fun (n : ℕ) => Phi (a (φ n)) (b (φ n))) Filter.atTop (nhds ((∑ i : Fin r, if A i.castSucc = 0 then -Real.logb 2 (d i) else sphericalEntropy ((A i.castSucc)⁻¹ - 1) - sphericalEntropy ((B i)⁻¹ - 1)) + sphericalEntropy ((A (Fin.last r))⁻¹ - 1)))

theorem MetricCodes.Spherical.HigherHierarchy.sum_neg_logb_eq_neg_logb_compactifiedEscapingRatioProduct {r k j : ℕ} (hkj : k + j = r) (d : Fin r → ℝ) (hd : ∀ (i : Fin r), ↑i < k → 0 < d i) : ∑ i : Fin k, -Real.logb 2 (d ⟨↑i, ⋯⟩) = -Real.logb 2 (MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct✝ hkj d)

theorem MetricCodes.Spherical.HigherHierarchy.forward_entropy_sum_eq_Phi_suffix_sub_logb_escaping_product {r k j : ℕ} (hkj : k + j = r) (A : Fin (r + 1) → ℝ) (B d : Fin r → ℝ) (hzero : ∀ (i : Fin r), A i.castSucc = 0 ↔ ↑i < k) (hd : ∀ (i : Fin r), ↑i < k → 0 < d i) : (∑ i : Fin r, if A i.castSucc = 0 then -Real.logb 2 (d i) else sphericalEntropy ((A i.castSucc)⁻¹ - 1) - sphericalEntropy ((B i)⁻¹ - 1)) + sphericalEntropy ((A (Fin.last r))⁻¹ - 1) = (Phi (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) - Real.logb 2 (MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct✝ hkj d)

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct_eq_filtered {r k j : ℕ} (hkj : k + j = r) (d : Fin r → ℝ) : MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct✝ hkj d = ∏ i : Fin r with ↑i < k, d i

theorem MetricCodes.Spherical.HigherHierarchy.compactified_entropy_sum_eq_residual_sub_logb {r k j q : ℕ} (hkj : k + j = r) (A : Fin (r + 1) → ℝ) (B d : Fin r → ℝ) (a₀ : Fin (q + 1) → ℝ) (b₀ : Fin q → ℝ) (c : ℝ) (hzero : ∀ (i : Fin r), A i.castSucc = 0 ↔ ↑i < k) (hd : ∀ (i : Fin r), ↑i < k → 0 < d i) (hresidualPhi : Phi a₀ b₀ = Phi (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) (hc : c = ∏ i : Fin r with ↑i < k, d i) : (∑ i : Fin r, if A i.castSucc = 0 then -Real.logb 2 (d i) else sphericalEntropy ((A i.castSucc)⁻¹ - 1) - sphericalEntropy ((B i)⁻¹ - 1)) + sphericalEntropy ((A (Fin.last r))⁻¹ - 1) = Phi a₀ b₀ - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.compactified_entropy_limit_eq_residual_sub_logb {r k j q : ℕ} (hkj : k + j = r) {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B d : Fin r → ℝ} {φ : ℕ → ℕ} {C L c : ℝ} (a₀ : Fin (q + 1) → ℝ) (b₀ : Fin q → ℝ) (hinter : ∀ (n : ℕ), Interlacing (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ C) (hA : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) (hB : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) (hAnonneg : ∀ (i : Fin (r + 1)), 0 ≤ A i) (hBnonneg : ∀ (i : Fin r), 0 ≤ B i) (hlast : 0 < A (Fin.last r)) (hratio : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) (hzero : ∀ (i : Fin r), A i.castSucc = 0 ↔ ↑i < k) (hd : ∀ (i : Fin r), ↑i < k → 0 < d i) (hlimit : Filter.Tendsto (fun (n : ℕ) => Phi (a (φ n)) (b (φ n))) Filter.atTop (nhds L)) (hresidualPhi : Phi a₀ b₀ = Phi (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) (hc : c = ∏ i : Fin r with ↑i < k, d i) : L = Phi a₀ b₀ - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.exists_forward_residual_entropy_of_closure_sequence {r : ℕ} {s R : ℝ} (u : ℕ → ℝ) (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) (hu : Filter.Tendsto u Filter.atTop (nhds s)) (hinter : ∀ (n : ℕ), Interlacing (a n) (b n)) (hgap : ∀ (n : ℕ), u n < 2 * Gamma (a n) (b n)) (hPhi : ∀ (n : ℕ), Phi (a n) (b n) ≤ R + 1 / (↑n + 1)) : ∃ (L : ℝ) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (d : Fin r → ℝ) (φ : ℕ → ℕ) (k : ℕ) (j : ℕ) (hkj : k + j = r) (q : ℕ) (a₀ : Fin (q + 1) → ℝ) (b₀ : Fin q → ℝ) (c : ℝ), StrictMono φ ∧ 0 ≤ L ∧ L ≤ R ∧ (∀ (i : Fin (r + 1)), A i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), B i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a (φ n) i)) Filter.atTop (nhds (A i))) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b (φ n) i)) Filter.atTop (nhds (B i))) ∧ Filter.Tendsto (fun (n : ℕ) => u (φ n)) Filter.atTop (nhds s) ∧ (∀ (n : ℕ), u (φ n) < 2 * Gamma (a (φ n)) (b (φ n))) ∧ Filter.Tendsto (fun (n : ℕ) => Phi (a (φ n)) (b (φ n))) Filter.atTop (nhds L) ∧ (∀ (i : Fin r), d i ∈ Set.Icc 0 1) ∧ (∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b (φ n) i / a (φ n) i.castSucc) Filter.atTop (nhds (d i))) ∧ (∀ (i : Fin r), A i.castSucc = 0 ↔ B i = 0) ∧ (∀ (i : Fin r), A i.castSucc = 0 → 0 < d i ∧ Filter.Tendsto (fun (n : ℕ) => b (φ n) i * (1 + b (φ n) i) / (a (φ n) i.castSucc * (1 + a (φ n) i.castSucc))) Filter.atTop (nhds (d i ^ 2))) ∧ q ≤ j ∧ Interlacing a₀ b₀ ∧ (∀ (i : Fin r), ↑i < k → A i.castSucc = 0 ∧ B i = 0) ∧ (∀ (i : Fin r), A i.castSucc = 0 ↔ ↑i < k) ∧ (∀ (i : Fin (j + 1)), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i ∈ Set.Ioc 0 1) ∧ (∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∈ Set.Ioc 0 1) ∧ (∀ (i : Fin j), MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.castSucc ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ∧ MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i ≤ MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i.succ) ∧ (Phi a₀ b₀ = Phi (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) ∧ (∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) (fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a₀ b₀ t) ∧ c = ∏ i : Fin r with ↑i < k, d i ∧ 0 < c ∧ c ≤ 1 ∧ (c < 1 → q < r) ∧ L = Phi a₀ b₀ - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.quadratic_residue_ratio_eq_normalized (x u v : ℝ) (hu : u ≠ 0) : (x - v * (1 + v)) / (x - u * (1 + u)) = (x * u⁻¹ ^ 2 - (v / u) ^ 2 - v / u * u⁻¹) / (x * u⁻¹ ^ 2 - 1 - u⁻¹)

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_quadratic_residue_ratio_of_degree_ratio {u v : ℕ → ℝ} {d : ℝ} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (hd : Filter.Tendsto (fun (k : ℕ) => v k / u k) Filter.atTop (nhds d)) (x : ℝ) : Filter.Tendsto (fun (k : ℕ) => (x - v k * (1 + v k)) / (x - u k * (1 + u k))) Filter.atTop (nhds (d ^ 2))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_one_sub_two_mul_Gamma_of_stieltjesPhaseProduct {r j : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) (A : Fin (j + 1) → ℝ) (B : Fin j → ℝ) (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hAB : Interlacing A B) (c : ℝ) (hproduct : ∀ (t : ℝ), 0 < t → Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds (c * stieltjesPhaseProduct A B t))) : Filter.Tendsto (fun (n : ℕ) => 1 - 2 * Gamma (a n) (b n)) Filter.atTop (nhds (c * (1 - 2 * Gamma A B)))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Gamma_of_stieltjesPhaseProduct {r j : ℕ} (a : ℕ → Fin (r + 1) → ℝ) (b : ℕ → Fin r → ℝ) (A : Fin (j + 1) → ℝ) (B : Fin j → ℝ) (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hAB : Interlacing A B) (c : ℝ) (hproduct : ∀ (t : ℝ), 0 < t → Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds (c * stieltjesPhaseProduct A B t))) : Filter.Tendsto (fun (n : ℕ) => Gamma (a n) (b n)) Filter.atTop (nhds ((1 - c) / 2 + c * Gamma A B))

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio_append {k r : ℕ} (u v : Fin k → ℝ) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (t : ℝ) : MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (Fin.append u a) (Fin.append v b) t = (∏ p : Fin k, (t + v p * (1 + v p)) / (t + u p * (1 + u p))) * MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a b t

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_quadraticCoordinate_of_tendsto {u : ℕ → ℝ} {x : ℝ} (hu : Filter.Tendsto u Filter.atTop (nhds x)) : Filter.Tendsto (fun (n : ℕ) => u n * (1 + u n)) Filter.atTop (nhds (x * (1 + x)))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjes_pair_factor_of_degree_ratio {u v : ℕ → ℝ} {d : ℝ} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (hd : Filter.Tendsto (fun (n : ℕ) => v n / u n) Filter.atTop (nhds d)) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => (t + v n * (1 + v n)) / (t + u n * (1 + u n))) Filter.atTop (nhds (d ^ 2))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_hierarchyStieltjesRatio_of_coordinatewise {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} (ha : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => a n i) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b n i) Filter.atTop (nhds (B i))) (hA : ∀ (i : Fin (r + 1)), 0 ≤ A i) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (a n) (b n) t) Filter.atTop (nhds (MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A B t))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_hierarchyStieltjesRatio_append_of_escaping {k r : ℕ} {u v : ℕ → Fin k → ℝ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} {d : Fin k → ℝ} (hu : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => u n i) Filter.atTop Filter.atTop) (hd : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => v n i / u n i) Filter.atTop (nhds (d i))) (ha : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => a n i) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b n i) Filter.atTop (nhds (B i))) (hA : ∀ (i : Fin (r + 1)), 0 ≤ A i) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (Fin.append (u n) (a n)) (Fin.append (v n) (b n)) t) Filter.atTop (nhds ((∏ i : Fin k, d i ^ 2) * MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A B t))

theorem MetricCodes.Spherical.HigherHierarchy.stieltjesPhaseProduct_eq_mul_hierarchyStieltjesRatio {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (t : ℝ) : stieltjesPhaseProduct a b t = t * MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ a b t

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjesPhaseProduct_append_of_escaping {k r : ℕ} {u v : ℕ → Fin k → ℝ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ} {d : Fin k → ℝ} (hu : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => u n i) Filter.atTop Filter.atTop) (hd : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => v n i / u n i) Filter.atTop (nhds (d i))) (ha : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => a n i) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b n i) Filter.atTop (nhds (B i))) (hA : ∀ (i : Fin (r + 1)), 0 ≤ A i) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (Fin.append (u n) (a n)) (Fin.append (v n) (b n)) t) Filter.atTop (nhds ((∏ i : Fin k, d i ^ 2) * stieltjesPhaseProduct A B t))

theorem MetricCodes.Spherical.HigherHierarchy.append_ambient_prefix_suffix {k r : ℕ} (a : Fin (k + r + 1) → ℝ) : (Fin.append (fun (i : Fin k) => a (Fin.castAdd (r + 1) i)) fun (i : Fin (r + 1)) => a (Fin.natAdd k i)) = a

theorem MetricCodes.Spherical.HigherHierarchy.append_stabilizer_prefix_suffix {k r : ℕ} (b : Fin (k + r) → ℝ) : (Fin.append (fun (i : Fin k) => b (Fin.castAdd r i)) fun (i : Fin r) => b (Fin.natAdd k i)) = b

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjesPhaseProduct_of_escaping_prefix {k r : ℕ} (a : ℕ → Fin (k + r + 1) → ℝ) (b : ℕ → Fin (k + r) → ℝ) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (d : Fin k → ℝ) (hu : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => a n (Fin.castAdd (r + 1) i)) Filter.atTop Filter.atTop) (hd : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => b n (Fin.castAdd r i) / a n (Fin.castAdd (r + 1) i)) Filter.atTop (nhds (d i))) (ha : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => a n (Fin.natAdd k i)) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b n (Fin.natAdd k i)) Filter.atTop (nhds (B i))) (hA : ∀ (i : Fin (r + 1)), 0 ≤ A i) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds ((∏ i : Fin k, d i ^ 2) * stieltjesPhaseProduct A B t))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjesPhaseProduct_of_escaping_prefix_strict_residual {k r q : ℕ} (a : ℕ → Fin (k + r + 1) → ℝ) (b : ℕ → Fin (k + r) → ℝ) (A : Fin (r + 1) → ℝ) (B : Fin r → ℝ) (A' : Fin (q + 1) → ℝ) (B' : Fin q → ℝ) (d : Fin k → ℝ) (hu : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => a n (Fin.castAdd (r + 1) i)) Filter.atTop Filter.atTop) (hd : ∀ (i : Fin k), Filter.Tendsto (fun (n : ℕ) => b n (Fin.castAdd r i) / a n (Fin.castAdd (r + 1) i)) Filter.atTop (nhds (d i))) (ha : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => a n (Fin.natAdd k i)) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => b n (Fin.natAdd k i)) Filter.atTop (nhds (B i))) (hA : ∀ (i : Fin (r + 1)), 0 ≤ A i) (hratio : ∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A B t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A' B' t) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds ((∏ i : Fin k, d i ^ 2) * stieltjesPhaseProduct A' B' t))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjesPhaseProduct_of_compactified_prefix {k r q : ℕ} (a : ℕ → Fin (k + r + 1) → ℝ) (b : ℕ → Fin (k + r) → ℝ) (A : Fin (k + r + 1) → ℝ) (B d : Fin (k + r) → ℝ) (A' : Fin (q + 1) → ℝ) (B' : Fin q → ℝ) (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hA : ∀ (i : Fin (k + r + 1)), A i ∈ Set.Icc 0 1) (ha : ∀ (i : Fin (k + r + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a n i)) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin (k + r)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b n i)) Filter.atTop (nhds (B i))) (hd : ∀ (i : Fin (k + r)), Filter.Tendsto (fun (n : ℕ) => b n i / a n i.castSucc) Filter.atTop (nhds (d i))) (hzero : ∀ (i : Fin k), A (Fin.castAdd (r + 1) i) = 0) (hpositiveA : ∀ (i : Fin (r + 1)), 0 < A (Fin.natAdd k i)) (hpositiveB : ∀ (i : Fin r), 0 < B (Fin.natAdd k i)) (hratio : ∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (fun (i : Fin (r + 1)) => (A (Fin.natAdd k i))⁻¹ - 1) (fun (i : Fin r) => (B (Fin.natAdd k i))⁻¹ - 1) t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A' B' t) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds ((∏ i : Fin k, d (Fin.castAdd r i) ^ 2) * stieltjesPhaseProduct A' B' t))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_stieltjesPhaseProduct_of_compactified_suffix {R k j q : ℕ} (hkj : k + j = R) (a : ℕ → Fin (R + 1) → ℝ) (b : ℕ → Fin R → ℝ) (A : Fin (R + 1) → ℝ) (B d : Fin R → ℝ) (A' : Fin (q + 1) → ℝ) (B' : Fin q → ℝ) (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hA : ∀ (i : Fin (R + 1)), A i ∈ Set.Icc 0 1) (ha : ∀ (i : Fin (R + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a n i)) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin R), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b n i)) Filter.atTop (nhds (B i))) (hd : ∀ (i : Fin R), Filter.Tendsto (fun (n : ℕ) => b n i / a n i.castSucc) Filter.atTop (nhds (d i))) (hzero : ∀ (i : Fin R), ↑i < k → A i.castSucc = 0) (hpositiveA : ∀ (i : Fin (j + 1)), 0 < MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i) (hpositiveB : ∀ (i : Fin j), 0 < MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i) (hratio : ∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) (fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A' B' t) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => stieltjesPhaseProduct (a n) (b n) t) Filter.atTop (nhds (MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct✝ hkj d ^ 2 * stieltjesPhaseProduct A' B' t))

theorem MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct_eq_filtered_prefix {R k j : ℕ} (hkj : k + j = R) (d : Fin R → ℝ) : MetricCodes.Spherical.HigherHierarchy.compactifiedEscapingRatioProduct✝ hkj d = ∏ i : Fin R with ↑i < k, d i

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_Gamma_of_compactified_suffix {R k j q : ℕ} (hkj : k + j = R) (a : ℕ → Fin (R + 1) → ℝ) (b : ℕ → Fin R → ℝ) (A : Fin (R + 1) → ℝ) (B d : Fin R → ℝ) (A' : Fin (q + 1) → ℝ) (B' : Fin q → ℝ) (c : ℝ) (h : ∀ (n : ℕ), Interlacing (a n) (b n)) (hAB : Interlacing A' B') (hA : ∀ (i : Fin (R + 1)), A i ∈ Set.Icc 0 1) (ha : ∀ (i : Fin (R + 1)), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (a n i)) Filter.atTop (nhds (A i))) (hb : ∀ (i : Fin R), Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.compactifiedHierarchyCoordinate✝ (b n i)) Filter.atTop (nhds (B i))) (hd : ∀ (i : Fin R), Filter.Tendsto (fun (n : ℕ) => b n i / a n i.castSucc) Filter.atTop (nhds (d i))) (hzero : ∀ (i : Fin R), ↑i < k → A i.castSucc = 0) (hpositiveA : ∀ (i : Fin (j + 1)), 0 < MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i) (hpositiveB : ∀ (i : Fin j), 0 < MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i) (hratio : ∀ (t : ℝ), 0 < t → MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ (fun (i : Fin (j + 1)) => (MetricCodes.Spherical.HigherHierarchy.compactifiedAmbientSuffix✝ hkj A i)⁻¹ - 1) (fun (i : Fin j) => (MetricCodes.Spherical.HigherHierarchy.compactifiedStabilizerSuffix✝ hkj B i)⁻¹ - 1) t = MetricCodes.Spherical.HigherHierarchy.hierarchyStieltjesRatio✝ A' B' t) (hc : c = ∏ i : Fin R with ↑i < k, d i) : Filter.Tendsto (fun (n : ℕ) => Gamma (a n) (b n)) Filter.atTop (nhds ((1 - c ^ 2) / 2 + c ^ 2 * Gamma A' B'))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_certificate_slack_of_strictMono {φ : ℕ → ℕ} (hφ : StrictMono φ) : Filter.Tendsto (fun (n : ℕ) => 1 / (↑(φ n) + 1)) Filter.atTop (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.compactified_certificate_entropy_le {r : ℕ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {φ : ℕ → ℕ} {R L : ℝ} (hφ : StrictMono φ) (hbound : ∀ (n : ℕ), Phi (a n) (b n) ≤ R + 1 / (↑n + 1)) (hlimit : Filter.Tendsto (fun (n : ℕ) => Phi (a (φ n)) (b (φ n))) Filter.atTop (nhds L)) : L ≤ R

theorem MetricCodes.Spherical.HigherHierarchy.compactified_certificate_threshold_le {r : ℕ} {u : ℕ → ℝ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {φ : ℕ → ℕ} {s Q : ℝ} (hφ : StrictMono φ) (hthreshold : Filter.Tendsto u Filter.atTop (nhds s)) (hfeasible : ∀ (n : ℕ), u n < 2 * Gamma (a n) (b n)) (hspectral : Filter.Tendsto (fun (n : ℕ) => Gamma (a (φ n)) (b (φ n))) Filter.atTop (nhds Q)) : s ≤ 2 * Q

theorem MetricCodes.Spherical.HigherHierarchy.compactified_certificate_residual_threshold_le {r j : ℕ} {u : ℕ → ℝ} {a : ℕ → Fin (r + 1) → ℝ} {b : ℕ → Fin r → ℝ} {A : Fin (j + 1) → ℝ} {B : Fin j → ℝ} {φ : ℕ → ℕ} {s c : ℝ} (hφ : StrictMono φ) (hthreshold : Filter.Tendsto u Filter.atTop (nhds s)) (hfeasible : ∀ (n : ℕ), u n < 2 * Gamma (a n) (b n)) (hspectral : Filter.Tendsto (fun (n : ℕ) => Gamma (a (φ n)) (b (φ n))) Filter.atTop (nhds ((1 - c ^ 2) / 2 + c ^ 2 * Gamma A B))) : s ≤ 1 - c ^ 2 * (1 - 2 * Gamma A B)

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelCompactifiedCertificateClosure_of_forward_residual_and_realization {r : ℕ} (hforward : MetricCodes.Spherical.HigherHierarchy.FixedLevelForwardCompactifiedResidualLimit✝ r) (hrealize : ∀ {j : ℕ} {s c : ℝ} (A : Fin (j + 1) → ℝ) (B : Fin j → ℝ), 0 < s → s < 1 → 0 < c → c ≤ 1 → Interlacing A B → s ≤ 1 - c ^ 2 * (1 - 2 * Gamma A B) → c = 1 ∧ j ≤ r ∨ c < 1 ∧ j + 1 ≤ r → levelRate r s ≤ Phi A B - Real.logb 2 c) : MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelCompactifiedCertificateClosure_of_forward_residual {r : ℕ} (hforward : MetricCodes.Spherical.HigherHierarchy.FixedLevelForwardCompactifiedResidualLimit✝ r) : MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelForwardCompactifiedResidualLimit (r : ℕ) : MetricCodes.Spherical.HigherHierarchy.FixedLevelForwardCompactifiedResidualLimit✝ r

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelCompactifiedCertificateClosure (r : ℕ) : MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_succ_lt_of_compactified_positive_minimizer {r j : ℕ} {s c : ℝ} {a : Fin (j + 1) → ℝ} {b : Fin j → ℝ} (hj : j ≤ r) (hc : 0 < c) (hc' : c ≤ 1) (hdrop : c < 1 → j < r) (h : Interlacing a b) (hlast : 0 < a (Fin.last j)) (hfeasible : s ≤ 1 - c ^ 2 * (1 - 2 * Gamma a b)) (hmin : levelRate r s = Phi a b - Real.logb 2 c) (htransfer : ∀ {k j' : ℕ} (A : Fin (j' + 1) → ℝ) (B : Fin j' → ℝ), Interlacing A B → s < 1 - c ^ 2 * (1 - 2 * Gamma A B) → c = 1 ∧ j' ≤ k ∨ c < 1 ∧ j' + 1 ≤ k → levelRate k s ≤ Phi A B - Real.logb 2 c) : levelRate (r + 1) s < levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.log_inv_lt_half_inv_sub_self {t : ℝ} (ht : 0 < t) (ht' : t < 1) : Real.log (1 / t) < (1 / t - t) / 2

theorem MetricCodes.Spherical.HigherHierarchy.lt_log_one_add_add_half_log_one_add_sq {t : ℝ} (ht : 0 < t) (ht' : t < 1) : t < Real.log (1 + t) + 1 / 2 * Real.log (1 + t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.classicalThreshold_entropy_lt_half_neg_logb {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalEntropy (classicalThreshold s) < -(1 / 2) * Real.logb 2 (1 - s)

theorem MetricCodes.Spherical.HigherHierarchy.compactified_zero_residual_cost_le {s c : ℝ} (_hs : 0 < s) (_hs' : s < 1) (hc : 0 < c) (hfeasible : s ≤ 1 - c ^ 2) : -(1 / 2) * Real.logb 2 (1 - s) ≤ -Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.classicalThreshold_entropy_lt_neg_logb_of_compactified_zero {s c : ℝ} (hs : 0 < s) (hs' : s < 1) (hc : 0 < c) (hfeasible : s ≤ 1 - c ^ 2) : sphericalEntropy (classicalThreshold s) < -Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_le_entropy_of_classicalThreshold_lt {s a : ℝ} (hs : 0 < s) (hs' : s < 1) (ha : classicalThreshold s < a) : levelRate 0 s ≤ sphericalEntropy a

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_eq_classical_of_pos {s : ℝ} (hs : 0 < s) (hs' : s < 1) : levelRate 0 s = sphericalEntropy (classicalThreshold s)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_eq_classical {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) : levelRate 0 s = sphericalEntropy (classicalThreshold s)

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactified_levelRate_minimizer {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : ∃ (j : ℕ) (c : ℝ) (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ), 0 < c ∧ c ≤ 1 ∧ Interlacing a b ∧ (c = 1 ∧ j ≤ r ∨ c < 1 ∧ j + 1 ≤ r) ∧ s ≤ 1 - c ^ 2 * (1 - 2 * Gamma a b) ∧ levelRate r s = Phi a b - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.exists_compactified_positive_levelRate_minimizer {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : ∃ (j : ℕ) (c : ℝ) (a : Fin (j + 1) → ℝ) (b : Fin j → ℝ), j ≤ r ∧ 0 < c ∧ c ≤ 1 ∧ (c < 1 → j < r) ∧ Interlacing a b ∧ 0 < a (Fin.last j) ∧ s ≤ 1 - c ^ 2 * (1 - 2 * Gamma a b) ∧ levelRate r s = Phi a b - Real.logb 2 c

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_succ_lt {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : levelRate (r + 1) s < levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective_continuous (s : ℝ) : Continuous fun (a : ℝ) => MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a

theorem MetricCodes.Spherical.HigherHierarchy.boundaryQuadratic_classicalThreshold_eq_zero {s : ℝ} (hs : 0 < s) (hs' : s < 1) : boundaryQuadratic s (classicalThreshold s) = 0

theorem MetricCodes.Spherical.HigherHierarchy.boundaryDegree_classicalThreshold_eq_zero {s : ℝ} (hs : 0 < s) (hs' : s < 1) : boundaryDegree s (classicalThreshold s) = 0

theorem MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective_classicalThreshold {s : ℝ} (hs : 0 < s) (hs' : s < 1) : MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s (classicalThreshold s) = sphericalEntropy (classicalThreshold s)

theorem MetricCodes.Spherical.HigherHierarchy.boundaryDegree_spectral_eq {s a : ℝ} (ha : 0 < a) (hquadratic : 0 ≤ boundaryQuadratic s a) : 2 * MetricCodes.Gamma a (boundaryDegree s a) = s

theorem MetricCodes.Spherical.HigherHierarchy.exists_variationalRate_boundary_minimizer_of_limit {s L : ℝ} (hs : 0 < s) (hs' : s < 1) (hlimit : Filter.Tendsto (fun (a : ℝ) => MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a) Filter.atTop (nhds L)) (hendpoint : sphericalEntropy (classicalThreshold s) < L) : ∃ (a : ℝ), classicalThreshold s < a ∧ variationalRate s = MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ∧ ∀ (t : ℝ), classicalThreshold s < t → MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ≤ MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s t

theorem MetricCodes.Spherical.HigherHierarchy.exists_variationalRate_boundary_minimizer_of_boundary_limit {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlimit : Filter.Tendsto (fun (a : ℝ) => MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a) Filter.atTop (nhds (-(1 / 2) * Real.logb 2 (1 - s)))) : ∃ (a : ℝ), classicalThreshold s < a ∧ variationalRate s = MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ∧ ∀ (t : ℝ), classicalThreshold s < t → MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ≤ MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s t

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_one_lt_variationalRate_of_boundary_minimizer {s a : ℝ} (hs : 0 < s) (hs' : s < 1) (hthreshold : classicalThreshold s < a) (hmin : variationalRate s = MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a) : levelRate 1 s < variationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.exists_variationalRate_boundary_minimizer {s : ℝ} (hs : 0 < s) (hs' : s < 1) : ∃ (a : ℝ), classicalThreshold s < a ∧ variationalRate s = MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ∧ ∀ (t : ℝ), classicalThreshold s < t → MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s a ≤ MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ s t

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_one_lt_variationalRate {s : ℝ} (hs : 0 < s) (hs' : s < 1) : levelRate 1 s < variationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.classicalHierarchyProfile_continuousOn_Icc {s : ℝ} (hs : s < 1) : ContinuousOn (fun (t : ℝ) => sphericalEntropy (classicalThreshold t)) (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_continuousOn_Icc {s : ℝ} (hs : s < 1) : ContinuousOn (levelRate 0) (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.levelRate_zero_lowerSemicontinuousOn_Icc {s : ℝ} (hs : s < 1) : LowerSemicontinuousOn (levelRate 0) (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_classical_minimizer {s : ℝ} (hs : 0 < s) (hs' : s < 1) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope (levelRate 0) s = levelRate 0 t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.localizedEnvelope_lt_of_positive_minimizer {κ κ' : ℝ → ℝ} {s : ℝ} (hs' : s < 1) (hκ' : ∀ t ∈ Set.Icc 0 s, 0 ≤ κ' t) (hmin : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t) (hstrict : ∀ t ∈ Set.Ioc 0 s, κ' t < κ t) : SidelnikovLocalization.localizedEnvelope κ' s < SidelnikovLocalization.localizedEnvelope κ s

theorem MetricCodes.Spherical.HigherHierarchy.localizedEnvelope_levelRate_succ_lt_of_lowerSemicontinuous {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlsc : LowerSemicontinuousOn (levelRate r) (Set.Icc 0 s)) (hstrict : ∀ t ∈ Set.Ioc 0 s, levelRate (r + 1) t < levelRate r t) : SidelnikovLocalization.localizedEnvelope (levelRate (r + 1)) s < SidelnikovLocalization.localizedEnvelope (levelRate r) s

theorem MetricCodes.Spherical.HigherHierarchy.localizedEnvelope_levelRate_lt_profile_of_positive_minimizer {r : ℕ} {κ : ℝ → ℝ} {s : ℝ} (hs' : s < 1) (hmin : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope κ s = κ t + SidelnikovLocalization.sliceCost s t) (hstrict : ∀ t ∈ Set.Ioc 0 s, levelRate r t < κ t) : SidelnikovLocalization.localizedEnvelope (levelRate r) s < SidelnikovLocalization.localizedEnvelope κ s

theorem MetricCodes.Spherical.HigherHierarchy.rowVariationalRate_nonneg_all (s : ℝ) : 0 ≤ variationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.rowVariationalRate_zero : variationalRate 0 = 0

theorem MetricCodes.Spherical.HigherHierarchy.eventually_rowVariationalRate_le_squared_entropy : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), variationalRate t ≤ sphericalEntropy (t ^ 2)

theorem MetricCodes.Spherical.HigherHierarchy.exists_positive_localized_row_minimizer_of_lowerSemicontinuous {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlsc : LowerSemicontinuousOn variationalRate (Set.Icc 0 s)) : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope variationalRate s = variationalRate t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.localized_level_one_lt_row_of_lowerSemicontinuous {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlsc : LowerSemicontinuousOn variationalRate (Set.Icc 0 s)) : SidelnikovLocalization.localizedEnvelope (levelRate 1) s < SidelnikovLocalization.localizedEnvelope variationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.localized_row_lt_level_zero_of_positive_minimizer {s : ℝ} (hs' : s < 1) (hmin : ∃ t ∈ Set.Ioc 0 s, SidelnikovLocalization.localizedEnvelope (levelRate 0) s = levelRate 0 t + SidelnikovLocalization.sliceCost s t) : SidelnikovLocalization.localizedEnvelope variationalRate s < SidelnikovLocalization.localizedEnvelope (levelRate 0) s

theorem MetricCodes.Spherical.HigherHierarchy.localized_row_lt_level_zero {s : ℝ} (hs : 0 < s) (hs' : s < 1) : SidelnikovLocalization.localizedEnvelope variationalRate s < SidelnikovLocalization.localizedEnvelope (levelRate 0) s

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_boundaryDegree_div_of_tendsto {u a : ℕ → ℝ} {s : ℝ} (hu : Filter.Tendsto u Filter.atTop (nhds s)) (ha : Filter.Tendsto a Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => boundaryDegree (u n) (a n) / a n) Filter.atTop (nhds √(1 - s))

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_boundaryDegree_atTop_of_tendsto {u a : ℕ → ℝ} {s : ℝ} (hs : s < 1) (hu : Filter.Tendsto u Filter.atTop (nhds s)) (ha : Filter.Tendsto a Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => boundaryDegree (u n) (a n)) Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_sphericalEntropy_sub_of_sequential_ratio {a b : ℕ → ℝ} {c : ℝ} (hc : 0 < c) (ha : Filter.Tendsto a Filter.atTop Filter.atTop) (hb : Filter.Tendsto b Filter.atTop Filter.atTop) (hratio : Filter.Tendsto (fun (n : ℕ) => b n / a n) Filter.atTop (nhds c)) : Filter.Tendsto (fun (n : ℕ) => sphericalEntropy (a n) - sphericalEntropy (b n)) Filter.atTop (nhds (-Real.logb 2 c))

theorem MetricCodes.Spherical.HigherHierarchy.CompactificationEntropy.tendsto_entropy_sub_boundaryDegree_of_tendsto {u a : ℕ → ℝ} {s : ℝ} (_hs : 0 < s) (hs' : s < 1) (hu : Filter.Tendsto u Filter.atTop (nhds s)) (ha : Filter.Tendsto a Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => sphericalEntropy (a n) - sphericalEntropy (boundaryDegree (u n) (a n))) Filter.atTop (nhds (-(1 / 2) * Real.logb 2 (1 - s)))

theorem MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective_joint_continuous : Continuous fun (p : ℝ × ℝ) => MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ p.1 p.2

theorem MetricCodes.Spherical.HigherHierarchy.variationalRate_lowerSemicontinuousOn_Icc_of_jointEscape {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hescape : ∀ {u a : ℕ → ℝ} {t : ℝ}, 0 < t → t < 1 → Filter.Tendsto u Filter.atTop (nhds t) → Filter.Tendsto a Filter.atTop Filter.atTop → Filter.Tendsto (fun (n : ℕ) => MetricCodes.Spherical.HigherHierarchy.oneRowBoundaryObjective✝ (u n) (a n)) Filter.atTop (nhds (-(1 / 2) * Real.logb 2 (1 - t)))) : LowerSemicontinuousOn variationalRate (Set.Icc 0 s)

theorem MetricCodes.Spherical.HigherHierarchy.variationalRate_lowerSemicontinuousOn_Icc {s : ℝ} (hs : 0 < s) (hs' : s < 1) : LowerSemicontinuousOn variationalRate (Set.Icc 0 s)

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

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

Equations

• MetricCodes.Spherical.HigherHierarchy.closedHierarchyVariationalRate s = sInf (MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet✝ s)

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

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

Equations

• MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate s = Filter.limsup (fun (n : ℕ) => Real.logb 2 ↑(SpherePacking.sphericalCodeNumber n s).toNat / ↑n) Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyRateSet_subset_closedHierarchyRateSet (s : ℝ) : hierarchyRateSet s ⊆ MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet✝ s

theorem MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet_bddBelow (s : ℝ) : BddBelow (MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet✝ s)

theorem MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet_nonempty_of_interior {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (MetricCodes.Spherical.HigherHierarchy.closedHierarchyRateSet✝ s).Nonempty

theorem MetricCodes.Spherical.HigherHierarchy.exists_strict_hierarchy_refinement_of_closed {r : ℕ} {s : ℝ} (hs : 0 < s) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (hinterlacing : Interlacing a b) (hspectral : s ≤ 2 * Gamma a b) : ∃ (r' : ℕ) (A : Fin (r' + 1) → ℝ) (B : Fin r' → ℝ), Interlacing A B ∧ s < 2 * Gamma A B ∧ Phi A B < Phi a b

theorem MetricCodes.Spherical.HigherHierarchy.closedHierarchyVariationalRate_eq_hierarchyVariationalRate {s : ℝ} (hs : 0 < s) (hs' : s < 1) : closedHierarchyVariationalRate s = hierarchyVariationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeLogRate_nonneg (s : ℝ) (n : ℕ) : 0 ≤ Real.logb 2 ↑(SpherePacking.sphericalCodeNumber n s).toNat / ↑n

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate_le_of_eventually_exponential {s R : ℝ} (hR : 0 ≤ R) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(SpherePacking.sphericalCodeNumber n s).toNat < 2 ^ (R * ↑n)) : sphericalCodeRate s ≤ R

def MetricCodes.Spherical.HigherHierarchy.FixedLevelHierarchyCodeBound : Prop

The fixed level hierarchy code bound used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.eventually_sphericalCodeNumber_lt_hierarchyVariationalRate_of_code_bound (hcode : FixedLevelHierarchyCodeBound) {s ε : ℝ} (hs : 0 < s) (hs' : s < 1) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(SpherePacking.sphericalCodeNumber n s).toNat < 2 ^ ((hierarchyVariationalRate s + ε) * ↑n)

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate_le_closedHierarchyVariationalRate_of_code_bound (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalCodeRate s ≤ closedHierarchyVariationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor_pos {s t : ℝ} (hs : s < 1) (hts : t ≤ s) : 0 < MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor✝ s t

theorem MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor_sq {s t : ℝ} (hs : s < 1) (hts : t ≤ s) : MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor✝ s t ^ 2 = (1 - s) / (1 - t)

theorem MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor_lt_one {s t : ℝ} (hs : s < 1) (hts : t < s) : MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor✝ s t < 1

theorem MetricCodes.Spherical.HigherHierarchy.neg_logb_compactificationCapFactor_eq_sliceCost {s t : ℝ} (hs : s < 1) (hts : t ≤ s) : -Real.logb 2 (MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor✝ s t) = SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor_scaled_spectral {r : ℕ} {s t : ℝ} (hs : s < 1) (hts : t ≤ s) {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (hgap : t < 2 * Gamma a b) : s < 1 - MetricCodes.Spherical.HigherHierarchy.compactificationCapFactor✝ s t ^ 2 * (1 - 2 * Gamma a b)

theorem MetricCodes.Spherical.HigherHierarchy.levelRateSet_nonempty_of_mem_source_interval {r : ℕ} {s t : ℝ} (hs : 0 < s) (hs' : s < 1) (hts : t ≤ s) : (MetricCodes.Spherical.HigherHierarchy.levelRateSet✝ r t).Nonempty

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_levelRate {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : hierarchyVariationalRate s ≤ levelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_levelRate_add_sliceCost_of_transfer {r : ℕ} {s t : ℝ} (hs : 0 < s) (hs' : s < 1) (hts : t ≤ s) (htransfer : ∀ {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ}, Interlacing A B → t < 2 * Gamma A B → hierarchyVariationalRate s ≤ Phi A B + SidelnikovLocalization.sliceCost s t) : hierarchyVariationalRate s ≤ levelRate r t + SidelnikovLocalization.sliceCost s t

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_localizedEnvelope_of_transfer {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (htransfer : ∀ {t : ℝ}, 0 ≤ t → t < s → ∀ {A : Fin (r + 1) → ℝ} {B : Fin r → ℝ}, Interlacing A B → t < 2 * Gamma A B → hierarchyVariationalRate s ≤ Phi A B + SidelnikovLocalization.sliceCost s t) : hierarchyVariationalRate s ≤ SidelnikovLocalization.localizedEnvelope (levelRate r) s

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_localizedEnvelope_of_compactification (hcompact : MetricCodes.Spherical.HigherHierarchy.GenuineCompactifiedHierarchyTransfer✝) {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) : hierarchyVariationalRate s ≤ SidelnikovLocalization.localizedEnvelope (levelRate r) s

theorem MetricCodes.Spherical.HigherHierarchy.hierarchyVariationalRate_le_localizedHierarchyInf_of_compactification (hcompact : MetricCodes.Spherical.HigherHierarchy.GenuineCompactifiedHierarchyTransfer✝) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : hierarchyVariationalRate s ≤ sInf (Set.range fun (r : ℕ) => SidelnikovLocalization.localizedEnvelope (levelRate r) s)

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate_le_localizedHierarchyInf_of_compactification (hcode : FixedLevelHierarchyCodeBound) (hcompact : MetricCodes.Spherical.HigherHierarchy.GenuineCompactifiedHierarchyTransfer✝) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalCodeRate s ≤ sInf (Set.range fun (r : ℕ) => SidelnikovLocalization.localizedEnvelope (levelRate r) s)

theorem MetricCodes.Spherical.HigherHierarchy.genuineCompactifiedHierarchyTransfer : MetricCodes.Spherical.HigherHierarchy.GenuineCompactifiedHierarchyTransfer✝

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate_le_localizedHierarchyInf (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalCodeRate s ≤ sInf (Set.range fun (r : ℕ) => SidelnikovLocalization.localizedEnvelope (levelRate r) s)

noncomputable def MetricCodes.Spherical.HigherHierarchy.localizedLevelRate (r : ℕ) (s : ℝ) : ℝ

The localized level rate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.localizedLevelRate r s = MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope (MetricCodes.Spherical.HigherHierarchy.levelRate r) s

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

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

Equations

• MetricCodes.Spherical.HigherHierarchy.localizedHierarchyRate s = sInf (Set.range fun (r : ℕ) => MetricCodes.Spherical.HigherHierarchy.localizedLevelRate r s)

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

The localized row rate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.localizedRowRate s = MetricCodes.Spherical.SidelnikovLocalization.localizedEnvelope MetricCodes.Spherical.variationalRate s

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

The classical localized rate used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.localizedLevelRate_nonneg {r : ℕ} {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) : 0 ≤ localizedLevelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.localizedHierarchyRate_le_level {r : ℕ} {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) : localizedHierarchyRate s ≤ localizedLevelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.localizedHierarchyRate_lt_level_one_of_level_two {s : ℝ} (hs : 0 ≤ s) (hs' : s < 1) (hstrict : localizedLevelRate 2 s < localizedLevelRate 1 s) : localizedHierarchyRate s < localizedLevelRate 1 s

theorem MetricCodes.Spherical.HigherHierarchy.sphericalCodeRate_le_localizedHierarchyRate_of_codeBound (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : sphericalCodeRate s ≤ localizedHierarchyRate s

theorem MetricCodes.Spherical.HigherHierarchy.localizedLevelRate_zero_eq_classicalLocalizedRate {s : ℝ} (_hs : 0 ≤ s) (hs' : s < 1) : localizedLevelRate 0 s = classicalLocalizedRate s

theorem MetricCodes.Spherical.HigherHierarchy.localizedLevelRate_one_lt_localizedRowRate {s : ℝ} (hs : 0 < s) (hs' : s < 1) : localizedLevelRate 1 s < localizedRowRate s

theorem MetricCodes.Spherical.HigherHierarchy.localizedRowRate_lt_localizedLevelRate_zero {s : ℝ} (hs : 0 < s) (hs' : s < 1) : localizedRowRate s < localizedLevelRate 0 s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy_of_components {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hlevel : ∀ (r : ℕ), levelRate (r + 1) s < levelRate r s) (hlocalized : ∀ (r : ℕ), localizedLevelRate (r + 1) s < localizedLevelRate r s) (hcode : sphericalCodeRate s ≤ localizedHierarchyRate s) (hrow : localizedLevelRate 1 s < localizedRowRate s) (hclassical : localizedRowRate s < localizedLevelRate 0 s) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s

theorem MetricCodes.Spherical.HigherHierarchy.localizedLevelRate_succ_lt_of_compactifiedCertificateClosure {r : ℕ} {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hstrict : ∀ t ∈ Set.Ioc 0 s, levelRate (r + 1) t < levelRate r t) (hclosure : MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r) : localizedLevelRate (r + 1) s < localizedLevelRate r s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy_of_codeBound_pointwiseStrict_and_compactifiedClosure {s : ℝ} (hs : 0 < s) (hs' : s < 1) (hcode : FixedLevelHierarchyCodeBound) (hlevel : ∀ (r : ℕ) (t : ℝ), 0 < t → t ≤ s → levelRate (r + 1) t < levelRate r t) (hclosure : ∀ (r : ℕ), MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy_of_codeBound_strictLevelRates_and_compactifiedClosure (hcode : FixedLevelHierarchyCodeBound) (hlevel : ∀ (r : ℕ) {t : ℝ}, 0 < t → t < 1 → levelRate (r + 1) t < levelRate r t) (hclosure : ∀ (r : ℕ), MetricCodes.Spherical.HigherHierarchy.FixedLevelCompactifiedCertificateClosure✝ r) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy_of_fixedLevelCodeBound (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s

theorem MetricCodes.Spherical.HigherHierarchy.main_general_of_actualCodeBound (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ {r : ℕ} {R : ℝ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ), Interlacing a b → s < 2 * Gamma a b → Phi a b < R → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (R * ↑n)) ∧ sphericalCodeRate s ≤ closedHierarchyVariationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy_of_actualCodeBound (hcode : FixedLevelHierarchyCodeBound) {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s