AdaptiveMeshCounting.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Actual lifted mesh endpoints and finite spacing bounds. Endpoint sets are constructed from the exponential mesh, not supplied as count hypotheses.

theorem OAI.QuantitativeVanDerWaerden.finite_spacing_bound line 14

Source documentation

The elementary one-dimensional packing inequality, with both end points included. This formulation has no rounding loss in subsequent estimates.

theorem finite_spacing_bound (s : Finset ℝ) (δ : ℝ) (hδ : 0 ≤ δ) :
    ∀ u v : ℝ, u ≤ v →
    (∀ x ∈ s, u ≤ x ∧ x ≤ v) →
    (∀ x ∈ s, ∀ y ∈ s, x < y → δ ≤ y - x) →
    (s.card : ℝ) * δ ≤ v - u + δ := by
…

def OAI.QuantitativeVanDerWaerden.integerTranslatesBetween line 46
theorem OAI.QuantitativeVanDerWaerden.mem_integerTranslatesBetween line 50
theorem OAI.QuantitativeVanDerWaerden.integerTranslatesBetween_card line 65
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.left_lt_half line 92
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.contains_left line 98
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.centered_of_lift_mem line 101
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.label_of_lift_mem line 109
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.lifted_unique line 115
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.exists_lift_mem line 125
Source documentation
Every real lift belongs to an actual half-open lifted mesh cell.
```
theorem exists_lift_mem (x : ℝ) :
    ∃ (i : A.Label) (z : ℤ), A.Contains i (x - z) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.lifted_endpoint_gap line 130
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.right_is_lifted_endpoint line 142
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpointsBetween line 172
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.mem_endpointsBetween line 179
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.neighborhoodEndpoints line 202
Source documentation
The anchor's closed circle neighborhood, realized by one real interval. An integer translate leaves every label and every width unchanged.
```
noncomputable def neighborhoodEndpoints (i : A.Label) (z : ℤ) : Finset ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.neighborhoodEndpoints_card line 205
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.activeEndpoints line 239
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.activeEndpoints_spacing line 245
Source documentation
Active endpoints are separated globally, including across the circle cut: the complete cell starting at the first endpoint lies before the second.
```
theorem activeEndpoints_spacing (η u v : ℝ) {x y : ℝ}
    (hx : x ∈ A.activeEndpoints η u v) (hy : y ∈ A.activeEndpoints η u v)
    (hxy : x < y) : A.H * η / 4 ≤ y - x := by
…
```
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.activeEndpoints_card_bound line 263
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.thresholdPoints line 285
Source documentation
The only additional discontinuities of the truncated label are the two threshold points in each period. Equality at either threshold is retained.
```
noncomputable def thresholdPoints (η u v : ℝ) : Finset ℝ :=
…
```
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedBreakpoints line 289
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.thresholdPoints_card line 292
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedBreakpoints_card_bound line 300
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedBreakpoints_card line 314