UniformWeightedSectionError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An absorption threshold independent of the path envelopes

theorem OAI.PolycyclicRecognition.weighted_section_error_absorbed_uniform line 32

Source documentation

Choose the small bridge threshold before the subexponential path envelope. This order is needed when the path constants are only fixed after choosing the contact pivot.

theorem weighted_section_error_absorbed_uniform
    (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)
    : ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ (R : ℝ → ℝ),
      (∀ r, 0 ≤ R r) → HasSubexponentialUpperBound R →
      ∃ S : ℝ → ℝ, HasSubexponentialUpperBound S ∧
        ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
…

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

theorem OAI.PolycyclicRecognition.weighted_section_error_absorbed_sequence_uniform line 96

Source documentation

The same threshold is uniform over the scale sequence and every subexponential input envelope.

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

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