IntervalSineMargin.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.two_mul_le_sin_pi_mul line 7
theorem OAI.Problem337.sin_pi_mul_lower_of_margin line 14
Source documentation
Sine is uniformly bounded below away from both endpoints of the unit interval.
```
theorem sin_pi_mul_lower_of_margin {a x : ℝ} (ha : 0 ≤ a)
    (hlo : a ≤ x) (hhi : x ≤ 1-a) : 2*a ≤ Real.sin (Real.pi*x) := by
…
```

theorem OAI.Problem337.inner_interval_difference_margin line 25

Source documentation

The inner interval stays separated, in both cyclic directions, from its complement.

theorem inner_interval_difference_margin {δ a t x : ℝ} (_ha : 0 ≤ a)
    (htlo : a ≤ t) (hthi : t ≤ δ-a) (hxlo : δ ≤ x) (hxhi : x ≤ 1) :
    a ≤ x-t ∧ x-t ≤ 1-a := by
…

theorem OAI.Problem337.inner_interval_sine_lower line 32
Source documentation
A geometric-sum denominator for an inner-interval kernel is bounded away from zero at every point outside the target interval.
```
theorem inner_interval_sine_lower {δ a t x : ℝ} (ha : 0 ≤ a)
    (htlo : a ≤ t) (hthi : t ≤ δ-a) (hxlo : δ ≤ x) (hxhi : x ≤ 1) :
    2*a ≤ Real.sin (Real.pi*(x-t)) := by
…
```

theorem OAI.Problem337.inner_interval_inverse_sin_sq line 39

Source documentation

Squaring the reciprocal sine bound gives the standard pointwise Fejer leakage.

theorem inner_interval_inverse_sin_sq {δ a t x h : ℝ} (ha : 0 < a) (hh : 0 < h)
    (htlo : a ≤ t) (hthi : t ≤ δ-a) (hxlo : δ ≤ x) (hxhi : x ≤ 1) :
    1/(h*(Real.sin (Real.pi*(x-t)))^2) ≤ 1/(4*h*a^2) := by
…

def OAI.Problem337.innerGridInterval line 50
Source documentation
Natural lattice points in a half-open normalized interval.
```
def innerGridInterval (q : ℕ) (a b : ℝ) : Finset ℕ :=
…
```
lemma OAI.Problem337.innerGridInterval_mem line 53

theorem OAI.Problem337.innerGridInterval_card_bounds line 65

Source documentation

Rounding loses at most one lattice point from the expected interval length.

theorem innerGridInterval_card_bounds (q : ℕ) {a b : ℝ}
    (ha : 0 ≤ a) (hab : a ≤ b) :
    (b-a)*(q : ℝ)-1 ≤ ((innerGridInterval q a b).card : ℝ) ∧
      ((innerGridInterval q a b).card : ℝ) ≤ (b-a)*(q : ℝ)+1 := by
…

Mentions: OAI.Problem337.innerGridInterval

theorem OAI.Problem337.innerGridInterval_three_quarters line 86

Source documentation

The standard inner three-quarter interval has cardinality close to 3δq/4.

theorem innerGridInterval_three_quarters (q : ℕ) {δ : ℝ} (hδ : 0 ≤ δ) :
    3*δ*(q : ℝ)/4-1 ≤ ((innerGridInterval q (δ/8) (7*δ/8)).card : ℝ) ∧
      ((innerGridInterval q (δ/8) (7*δ/8)).card : ℝ) ≤ 3*δ*(q : ℝ)/4+1 := by
…

Mentions: OAI.Problem337.innerGridInterval