WeightedSectionError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The ideal coordinate after a small ambient logarithmic error

This is the last assertion of the manuscript's strict-width absorption lemma. The error factor is computed by BCH; its ideal part is absorbed by positive widths before multiplying the two ideal factors.

theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.eventually_le_perturbed_exp line 19

theorem OAI.PolycyclicRecognition.weighted_section_error_absorbed line 45

Source documentation

A subexponential full box followed by a small exponential error still has a subexponential ideal coordinate at the same positive widths.

theorem weighted_section_error_absorbed
    (cost : I → ℝ) {lo M : ℝ} (hlo : 0 < lo)
    (hcost : ∀ i, lo ≤ cost i) (hM : 0 < M)
    (C : ℝ) (hC : 0 ≤ C)
    (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 ∧
      ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
      ∀ ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
…

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