FiniteRootMesh.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite interval partition at every arithmetic root

theorem OAI.Ostmann.finite_root_mesh line 12

Source documentation

Partition a bounded interval at all roots in it, retaining the roots as endpoints. The number of intervals is at most the number of cuts plus one.

theorem finite_root_mesh (S : Finset ℝ) (u v : ℝ) (huv : u ≤ v) :
    ∃ (s : ℕ → ℝ) (N : ℕ), Monotone s ∧ s 0 = u ∧ s N = v ∧ N ≤ S.card + 1 ∧
      ∀ j < N, ∀ r ∈ S, r ∉ Set.Ioo (s j) (s (j + 1)) := by
…

theorem OAI.Ostmann.rootCellCode_eq_of_root_free line 69

Source documentation

The side of every root is constant in the open part of one partition cell.

theorem rootCellCode_eq_of_root_free (S : Finset ℝ) (a b x y : ℝ)
    (hfree : ∀ r ∈ S, r ∉ Set.Ioo a b)
    (hx : x ∈ Set.Ioo a b) (hy : y ∈ Set.Ioo a b) :
    rootCellCode S x = rootCellCode S y := by
…

Mentions: OAI.Ostmann.rootCellCode

theorem OAI.Ostmann.finite_log_root_mesh line 84

Source documentation

A partition in logarithmic coordinates still includes every positive root of the original giant-variable polynomials.

theorem finite_log_root_mesh (S : Finset ℝ) (u v : ℝ) (huv : u ≤ v) :
    ∃ (s : ℕ → ℝ) (N : ℕ), Monotone s ∧ s 0 = u ∧ s N = v ∧ N ≤ S.card + 1 ∧
      ∀ j < N, ∀ r ∈ S, r ∉ Set.Ioo (Real.exp (s j)) (Real.exp (s (j + 1))) := by
…