ScaleInduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QAC.finite_scale_induction line 13

Source documentation

Finite scale bootstrap, stated for the uniform bound relation. This is a pure real-arithmetic induction and contains no operator-theoretic assumption.

theorem finite_scale_induction (B : ℝ → ℝ → Prop)
    (large : ∀ s t, 0 ≤ s → s < t → 1 < t → B s t)
    (backstep : ∀ s t a b u w, 0 ≤ s → s < a → a < u → u < w → w < t → t < b →
      (a + b) / 2 < u → B t b → B s t) :
    ∀ s t, 0 ≤ s → s < t → B s t := by
…