SequenceWeightedSectionError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small-error absorption along the actual profile scale sequence

theorem OAI.PolycyclicRecognition.weighted_section_error_absorbed_sequence line 31

Source documentation

The absorption theorem requires only sequential subexponential data, with no regularity between the scale values.

theorem weighted_section_error_absorbed_sequence
    (scale : ℕ → ℝ) (hs : StrictMono scale) (hscale : Tendsto scale atTop atTop)
    (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 : ∀ n, 0 ≤ R n)
    (hRsub : HasSubexponentialUpperBoundSeq scale R) :
    ∃ S : ℕ → ℝ, HasSubexponentialUpperBoundSeq scale S ∧
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq