OAI/NumberTheory/Ostmann/ZeroDensity/IntervalDensityTree.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Equal subdivisions of actual intervals

Cumulative mass functions give exact averaging identities on the interval partition, so the density-increment tree applies to concrete interval masses.

  1. def OAI.Ostmann.intervalNode line 19
  2. def OAI.Ostmann.intervalNodeDensity line 22
  3. theorem OAI.Ostmann.intervalNode_nil line 27
  4. theorem OAI.Ostmann.intervalNode_child line 30
  5. theorem OAI.Ostmann.intervalNode_width_pos line 36
  6. theorem OAI.Ostmann.equal_interval_mass_sum line 44
  7. theorem OAI.Ostmann.intervalNodeDensity_average line 56
  8. theorem OAI.Ostmann.intervalNode_width line 70
  9. theorem OAI.Ostmann.intervalNode_bounds line 79
  10. theorem OAI.Ostmann.intervalNode_width_lower line 101
  11. theorem OAI.Ostmann.exists_rich_interval_node line 110

    Source documentation

    A concrete cumulative mass function has a rich interval node once its root density is positive and all relevant interval densities are bounded.

    theorem exists_rich_interval_node {M : ℕ} (hM : 0 < M) (H : ℕ)
    (φ : ℝ → ℝ) (a L d U : ℝ) (hL : 0 < L) (hd : 0 < d)
    (hroot : d ≤ (φ (a + L) - φ a) / L)
    (hupper : ∀ w : List (Fin M), w.length ≤ H → intervalNodeDensity φ a L w ≤ U)
    (hdepth : U < d + H * (d / (4 * M))) :
    ∃ w : List (Fin M), w.length < H ∧
      ∀ i, d / 2 ≤ intervalNodeDensity φ a L (w ++ [i]) := by
…

    Mentions: OAI.Ostmann.intervalNodeDensity