CoordinateCover.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TriangularCovering.η line 11
Also declared: ComparatorChallenges/CylinderCovering.lean:67 (same declaration text).
def OAI.TriangularCovering.alpha line 13
Also declared: ComparatorChallenges/CylinderCovering.lean:69 (same declaration text).
def OAI.TriangularCovering.beta line 15
Also declared: ComparatorChallenges/CylinderCovering.lean:71 (same declaration text).
def OAI.TriangularCovering.d line 17
Also declared: ComparatorChallenges/CylinderCovering.lean:73 (same declaration text).
theorem OAI.TriangularCovering.d_le_max_endpoints line 20
Source documentation
The maximum of d on an interval is attained at an endpoint.
```
theorem d_le_max_endpoints {a b q : ℝ} (ha : a ≤ q) (hb : q ≤ b) :
    d q ≤ max (d a) (d b) := by
…
```
Mentions: OAI.TriangularCovering.d
def OAI.TriangularCovering.cutoffCoeff line 40
Also declared: ComparatorChallenges/CylinderCovering.lean:75 (same declaration text).
theorem OAI.TriangularCovering.cutoffCoeff_eq_sSup line 42
theorem OAI.TriangularCovering.d_bounds line 59
theorem OAI.TriangularCovering.coeff_bounds line 66
theorem OAI.TriangularCovering.shared_left line 87
theorem OAI.TriangularCovering.shared_right line 90
theorem OAI.TriangularCovering.beta_error line 93
theorem OAI.TriangularCovering.alpha_error line 99

theorem OAI.TriangularCovering.first_crossing line 116

Source documentation

First crossing in a finite sequence; no monotonicity is required.

theorem first_crossing {N : ℕ} (hN : 0 < N) (f : ℕ → ℝ) (z : ℝ)
    (h0 : f 0 ≤ z) (hN' : z ≤ f N) :
    ∃ j : ℕ, j < N ∧ f j ≤ z ∧ z ≤ f (j + 1) := by
…

theorem OAI.TriangularCovering.rough_angle line 132

Source documentation

A uniform first-order estimate, used only after both cutoffs fail.

theorem rough_angle {ε x y q a r : ℝ} (he : 0 ≤ ε)
    (hx : |x| ≤ 1) (hq : |q| ≤ 1) (ha : |a| ≤ 1 / 2)
    (hr0 : 1 / 2 ≤ r) (hr1 : r ≤ 1 / 2 + ε / 2)
    (hy : y = r * q + ε * x * a) : |y - q / 2| ≤ ε := by
…

theorem OAI.TriangularCovering.rough_square line 152
theorem OAI.TriangularCovering.cross_term_bound line 165
theorem OAI.TriangularCovering.weighted_errors line 190

theorem OAI.TriangularCovering.radial_identity line 207

Source documentation

The exact cancellation which makes the secant construction work.

theorem radial_identity {ε x y q p a b β γ r s : ℝ}
    (hrs : r + s = 1 - ε * x * β + ε * y * γ)
    (hy : y = r * q + ε * x * a) (hx : x = s * p - ε * y * b) :
    (r - 1 / 2) * (1 - ε * x * q) + (s - 1 / 2) * (1 + ε * y * p) =
      ε ^ 2 * (x ^ 2 * a + y ^ 2 * b) - ε * x * (β - q / 2) + ε * y * (γ - p / 2) := by
…

theorem OAI.TriangularCovering.radial_lower_est line 219
theorem OAI.TriangularCovering.radial_failure line 226

theorem OAI.TriangularCovering.radial_exclusion line 260

Source documentation

Quantitative radial exclusion, with uniform constants independent of the mesh.

theorem radial_exclusion {ε Δ x y q p a b β γ M N r s : ℝ}
    (he0 : 0 < ε) (he1 : ε ≤ η / 2) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ ε ^ 2)
    (hxy : |x| + |y| ≤ 1) (hq : |q| ≤ 1) (hp : |p| ≤ 1)
    (ha0 : 0 ≤ a) (ha1 : a ≤ 1 / 2) (hb0 : 0 ≤ b) (hb1 : b ≤ 1 / 2)
    (hβ : |β| ≤ 1 / 2) (hγ : |γ| ≤ 1 / 2)
    (heβ : |β - q / 2| ≤ Δ / 4) (heγ : |γ - p / 2| ≤ Δ / 4)
    (hea : |a - (1 + q ^ 2) / 4| ≤ Δ / 2)
    (heb : |b - (1 + p ^ 2) / 4| ≤ Δ / 2)
    (hM : η + d q ≤ M) (hN : η + d p ≤ N)
    (hMN : M + N ≤ 1 / 4 + 2 * η)
    (hrs : r + s = 1 - ε * x * β + ε * y * γ)
    (hy : y = r * q + ε * x * a) (hx : x = s * p - ε * y * b) :
…

Mentions: OAI.TriangularCovering.η, OAI.TriangularCovering.d

def OAI.TriangularCovering.step line 306
Also declared: ComparatorChallenges/CylinderCovering.lean:77 (same declaration text).
def OAI.TriangularCovering.mesh line 308
Also declared: ComparatorChallenges/CylinderCovering.lean:79 (same declaration text).
theorem OAI.TriangularCovering.step_pos line 310
theorem OAI.TriangularCovering.mesh_zero line 314
theorem OAI.TriangularCovering.mesh_last line 316
theorem OAI.TriangularCovering.mesh_succ line 322
theorem OAI.TriangularCovering.mesh_abs_le line 326
def OAI.TriangularCovering.Sector line 341
Source documentation
Both closed angular inequalities, including a nonnegative radial coordinate.
```
def Sector (a b r z : ℝ) : Prop := 0 ≤ r ∧ a * r ≤ z ∧ z ≤ b * r
```
theorem OAI.TriangularCovering.angular_sector line 343
def OAI.TriangularCovering.cutoff line 374
Also declared: ComparatorChallenges/CylinderCovering.lean:81 (same declaration text).
theorem OAI.TriangularCovering.cutoff_pos line 376
theorem OAI.TriangularCovering.angle_in_interval line 382
theorem OAI.TriangularCovering.abs_le_of_interval line 386
theorem OAI.TriangularCovering.selected_cuts line 390
def OAI.TriangularCovering.LowerHit line 434
Source documentation
Coordinate form of membership in the first intercept cylinder.
```
def LowerHit (N j : ℕ) (ε x y t : ℝ) : Prop :=
…
```
def OAI.TriangularCovering.UpperHit line 441
Source documentation
Coordinate form of membership in the second intercept cylinder.
```
def UpperHit (N j : ℕ) (ε x y t : ℝ) : Prop :=
…
```

theorem OAI.TriangularCovering.finite_coordinate_cover line 448

Source documentation

Every boundary point is covered, not merely almost every point.

theorem finite_coordinate_cover {N : ℕ} {ε x y t : ℝ}
    (hN : 0 < N) (he0 : 0 < ε) (he1 : ε ≤ η / 2) (hmesh : step N ≤ ε ^ 2)
    (hx : |x| ≤ 1 - t) (hy : |y| ≤ t) :
    (∃ j : ℕ, j < N ∧ LowerHit N j ε x y t) ∨
    (∃ j : ℕ, j < N ∧ UpperHit N j ε x y t) := by
…

Mentions: OAI.TriangularCovering.η, OAI.TriangularCovering.step, OAI.TriangularCovering.LowerHit, OAI.TriangularCovering.UpperHit

theorem OAI.TriangularCovering.ceil_count_pos line 468
theorem OAI.TriangularCovering.ceil_step_le line 472

theorem OAI.TriangularCovering.finite_coordinate_cover_ceil line 480

Source documentation

Coverage with the exact ceiling count, in intercept coordinates.

theorem finite_coordinate_cover_ceil {ε x y t : ℝ}
    (he0 : 0 < ε) (he1 : ε ≤ η / 2) (hx : |x| ≤ 1 - t) (hy : |y| ≤ t) :
    (∃ j : ℕ, j < ⌈2 / ε ^ 2⌉₊ ∧ LowerHit ⌈2 / ε ^ 2⌉₊ j ε x y t) ∨
    (∃ j : ℕ, j < ⌈2 / ε ^ 2⌉₊ ∧ UpperHit ⌈2 / ε ^ 2⌉₊ j ε x y t) :=
…

Mentions: OAI.TriangularCovering.η, OAI.TriangularCovering.LowerHit, OAI.TriangularCovering.UpperHit

def OAI.TriangularCovering.speedSq line 491
Also declared: ComparatorChallenges/CylinderCovering.lean:83 (same declaration text).
def OAI.TriangularCovering.normalizedTerm line 493
Also declared: ComparatorChallenges/CylinderCovering.lean:85 (same declaration text).