RichSubintervals.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Every sufficiently long subinterval of a rich grid is rich

theorem OAI.Ostmann.grid_increment_lower line 11

theorem OAI.Ostmann.rich_grid_subinterval line 30

Source documentation

A monotone cumulative mass whose grid cells have density at least d has density at least d/2 on each internal interval at least four cells long.

theorem rich_grid_subinterval (φ : ℝ → ℝ) (hmono : Monotone φ)
    (M : ℕ) (a h d : ℝ) (hh : 0 < h) (hd : 0 ≤ d)
    (hstep : ∀ i : ℕ, i < M →
      d * h ≤ φ (a + ((i : ℝ) + 1) * h) - φ (a + (i : ℝ) * h))
    (u v : ℝ) (hau : a ≤ u) (huv : u ≤ v) (hvb : v ≤ a + M * h)
    (hlong : 4 * h ≤ v - u) :
    (d / 2) * (v - u) ≤ φ v - φ u := by
…

theorem OAI.Ostmann.cdf_interval_upper line 75

Source documentation

A uniform unit-interval mass bound gives a linear bound, with just one boundary interval of overhead.

theorem cdf_interval_upper (φ : ℝ → ℝ) (hmono : Monotone φ)
    (a₀ A : ℝ) (hA : 0 ≤ A)
    (hunit : ∀ a, a₀ ≤ a → φ (a + 1) - φ a ≤ A)
    (a b : ℝ) (ha : a₀ ≤ a) (hab : a ≤ b) :
    φ b - φ a ≤ A * (b - a + 1) := by
…

theorem OAI.Ostmann.exists_dense_fixed_block line 97

Source documentation

A long interval of positive density contains a whole block of any prescribed fixed length with at least half that density. The only loss is the final incomplete block.

theorem exists_dense_fixed_block (φ : ℝ → ℝ) (a L B d A : ℝ)
    (hL : 0 ≤ L) (hB : 0 < B) (hd : 0 < d) (hA : 0 ≤ A)
    (hupper : ∀ u v, a ≤ u → u ≤ v → v ≤ a + L →
      φ v - φ u ≤ A * (v - u + 1))
    (hroot : d * L ≤ φ (a + L) - φ a)
    (hlarge : 2 * A * (B + 1) < d * L) :
    ∃ b, a ≤ b ∧ b + B ≤ a + L ∧ (d / 2) * B ≤ φ (b + B) - φ b := by
…

theorem OAI.Ostmann.rich_interval_node_subinterval line 130