SeparatedIntervalCount.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.separated_interval_card line 10

Source documentation

Packing bound for integer-indexed values separated at a positive linear rate.

theorem separated_interval_card (s : Finset ℤ) (f : ℤ → ℝ)
    (lam u v : ℝ) (hlam : 0 < lam) (huv : u ≤ v)
    (hsep : ∀ i ∈ s, ∀ j ∈ s, i ≤ j → lam * ((j : ℝ) - i) ≤ f j - f i)
    (hrange : ∀ i ∈ s, u ≤ f i ∧ f i ≤ v) :
    (s.card : ℝ) ≤ (v - u) / lam + 1 := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.separated_near_integer_card line 45

Source documentation

The number of separated samples near integers is controlled by the number of integer centers and the packing bound in each short interval.

theorem separated_near_integer_card (s : Finset ℤ) (f : ℤ → ℝ)
    (lam β L U : ℝ) (hlam : 0 < lam) (hβ : 0 ≤ β) (hLU : L ≤ U)
    (hsep : ∀ i ∈ s, ∀ j ∈ s, i ≤ j → lam * ((j : ℝ) - i) ≤ f j - f i)
    (hrange : ∀ i ∈ s, L ≤ f i ∧ f i ≤ U) :
    ((s.filter fun i => ∃ q : ℤ, |f i - q| ≤ β).card : ℝ) ≤
      (U - L + 2 * β + 1) * (2 * β / lam + 1) := by
…

theorem OAI.Problem337.separated_near_integer_card_nat line 96

Source documentation

Natural-index version for finite exponential-sum blocks.

theorem separated_near_integer_card_nat (s : Finset ℕ) (f : ℕ → ℝ)
    (lam β L U : ℝ) (hlam : 0 < lam) (hβ : 0 ≤ β) (hLU : L ≤ U)
    (hsep : ∀ i ∈ s, ∀ j ∈ s, i ≤ j → lam * ((j : ℝ) - i) ≤ f j - f i)
    (hrange : ∀ i ∈ s, L ≤ f i ∧ f i ≤ U) :
    ((s.filter fun i : ℕ => ∃ q : ℤ, |f i - q| ≤ β).card : ℝ) ≤
      (U - L + 2 * β + 1) * (2 * β / lam + 1) := by
…

theorem OAI.Problem337.slope_bounds_of_adjacent line 117

Source documentation

Adjacent slope bounds telescope to bounds between arbitrary indices.

theorem slope_bounds_of_adjacent (f : ℕ → ℝ) (N : ℕ) (lam B : ℝ)
    (hstep : ∀ j < N, lam ≤ f (j + 1) - f j ∧ f (j + 1) - f j ≤ B) :
    ∀ j ≤ N, ∀ i ≤ j,
      lam * ((j : ℝ) - i) ≤ f j - f i ∧
      f j - f i ≤ B * ((j : ℝ) - i) := by
…

theorem OAI.Problem337.adjacent_near_integer_card line 141

Source documentation

Direct interface for the bad part of the discrete second-derivative test.

theorem adjacent_near_integer_card (f : ℕ → ℝ) (N : ℕ) (lam B β : ℝ)
    (hlam : 0 < lam) (hB : 0 ≤ B) (hβ : 0 ≤ β)
    (hstep : ∀ j < N, lam ≤ f (j + 1) - f j ∧ f (j + 1) - f j ≤ B) :
    (((Finset.range N).filter fun i => ∃ q : ℤ, |f i - q| ≤ β).card : ℝ) ≤
      (B * N + 2 * β + 1) * (2 * β / lam + 1) := by
…

theorem OAI.Problem337.derivative_near_integer_card line 164

Source documentation

Continuous derivative hypotheses imply the discrete separation needed for near-integer counting on any finite set of integer sample points.

theorem derivative_near_integer_card (s : Finset ℤ) (g : ℝ → ℝ)
    (a b lam B β : ℝ) (hab : a ≤ b) (hlam : 0 < lam) (hβ : 0 ≤ β)
    (hg : ContinuousOn g (Set.Icc a b))
    (hg' : DifferentiableOn ℝ g (interior (Set.Icc a b)))
    (hderiv : ∀ x ∈ interior (Set.Icc a b), lam ≤ deriv g x ∧ deriv g x ≤ B)
    (hs : ∀ i ∈ s, (i : ℝ) ∈ Set.Icc a b) :
    ((s.filter fun i : ℤ => ∃ q : ℤ, |g (i : ℝ) - q| ≤ β).card : ℝ) ≤
      (B * (b - a) + 2 * β + 1) * (2 * β / lam + 1) := by
…

theorem OAI.Problem337.near_integer_sqrt_budget line 198

Source documentation

The square-root choice in the second-derivative estimate gives the expected three-term shape, with explicit harmless constants.

theorem near_integer_sqrt_budget (A T lam : ℝ) (hA : 0 ≤ A) (hT : 0 ≤ T)
    (hlam : 0 < lam) (hlam1 : lam ≤ 1) :
    (A * lam * T + 2 * Real.sqrt lam + 1) * (2 * Real.sqrt lam / lam + 1) ≤
      3 * A * T * Real.sqrt lam + 2 / Real.sqrt lam + 7 := by
…