SectionErrorAbsorption.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Small logarithmic errors in ideal-section coordinates

theorem OAI.PolycyclicRecognition.section_error_absorbed line 33

Source documentation

The ideal error created by a pure section followed by a small ambient error is absorbed by every strictly positive ideal width.

theorem section_error_absorbed (C : ℝ) (hC : 0 ≤ C)
    (hbr : ∀ i j k, |(B).repr ⁅B i, B j⁆ k| ≤ C)
    (cost : I → ℝ) {lo α : ℝ} (hcost : ∀ i, lo ≤ cost i) (hα : 0 ≤ α)
    (hgap : ((c * c : ℕ) : ℝ) * α < lo)
    (ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) :
    ∀ᶠ r in atTop, ∀ (q : V ⧸ U.toSubmodule) (e : V),
      ‖bQ.equivFun q‖ ≤ Real.exp ((α + ε r) * r) →
      ‖(B).equivFun e‖ ≤ Real.exp ((α + ε r) * r) →
      ∃ (u : U) (q' : V ⧸ U.toSubmodule),
        ExpN (quotientLinearSection U bQ lift q) * ExpN e =
          ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q') ∧
        ‖(exponentialRescaleBasis bI cost r).equivFun u‖ ≤ 1 := by
…

Mentions: OAI.PolycyclicRecognition.quotientLinearSection, OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.exists_section_error_absorption_threshold line 59

Source documentation

One positive threshold works for all error envelopes. It depends only on the least ideal width, the BCH degree and the fixed error exponent.

theorem exists_section_error_absorption_threshold (C : ℝ) (hC : 0 ≤ C)
    (hbr : ∀ i j k, |(B).repr ⁅B i, B j⁆ k| ≤ C)
    (cost : I → ℝ) {lo M : ℝ} (hlo : 0 < lo) (hcost : ∀ i, lo ≤ cost i)
    (hM : 0 < M) :
    ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
      ∀ ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
      ∀ᶠ r in atTop, ∀ (q : V ⧸ U.toSubmodule) (e : V),
        ‖bQ.equivFun q‖ ≤ Real.exp ((M * δ + ε r) * r) →
        ‖(B).equivFun e‖ ≤ Real.exp ((M * δ + ε r) * r) →
        ∃ (u : U) (q' : V ⧸ U.toSubmodule),
          ExpN (quotientLinearSection U bQ lift q) * ExpN e =
            ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q') ∧
…

Mentions: OAI.PolycyclicRecognition.quotientLinearSection

theorem OAI.PolycyclicRecognition.section_box_subexponential_envelope line 89

Source documentation

Polynomial losses in the adapted box comparison are subexponential.

theorem section_box_subexponential_envelope (C : ℝ) (hC : 0 ≤ C)
    (R : ℝ → ℝ) (hR : ∀ r, 0 ≤ R r) (hRsub : HasSubexponentialUpperBound R) :
    HasSubexponentialUpperBound (fun r => K C * (1 + R r) ^ c) := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBound

theorem OAI.PolycyclicRecognition.section_box_comparison line 100

Source documentation

The two inclusions in the ideal-section box comparison share a single subexponential envelope. The quotient has exactly the zero-width coordinates.

theorem section_box_comparison (C : ℝ) (hC : 0 ≤ C) (cost : I → ℝ)
    (hbr : ∀ r : ℝ, 0 ≤ r → ∀ i j k,
      |(exponentialRescaleBasis B (Sum.elim cost (fun _ => 0)) r).repr
        ⁅exponentialRescaleBasis B (Sum.elim cost (fun _ => 0)) r i,
          exponentialRescaleBasis B (Sum.elim cost (fun _ => 0)) r j⁆ k| ≤ C)
    (R : ℝ → ℝ) (hR : ∀ r, 0 ≤ R r) (hRsub : HasSubexponentialUpperBound R) :
    ∃ S : ℝ → ℝ, HasSubexponentialUpperBound S ∧ ∀ r : ℝ, 0 ≤ r →
      (∀ n : N, n ∈ exponentialCoordinateBox ExpN
          (exponentialRescaleBasis B (Sum.elim cost (fun _ => 0)) r) (R r) →
        ∃ (u : U) (q : V ⧸ U.toSubmodule),
          n = ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q) ∧
          ‖(exponentialRescaleBasis bI cost r).equivFun u‖ ≤ S r ∧
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.HasSubexponentialUpperBound, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.quotientLinearSection