ScalarAdaptiveMesh.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The adaptive mesh with the selected scalar parameters

This adapter instantiates the proved adaptive-mesh construction with H=k⁻² and alpha=q^(-(D+1)). Its interval count agrees with the scalar ceiling used in the numerical size estimates.

theorem OAI.QuantitativeVanDerWaerden.Parameters.selected_meshScale_le_eighth line 18
theorem OAI.QuantitativeVanDerWaerden.Parameters.selected_meshScale_le_one line 26
def OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh line 30
Source documentation
The actual exponential mesh for the selected progression length and base.
```
def selectedAdaptiveMesh {k q : ℕ} (hk : 3 ≤ k) (hq : 2 ≤ q) : AdaptiveMesh where
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh
theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_H line 38
theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_alpha line 41
theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_R line 44
theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_m line 47
theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_card line 54

theorem OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh_card_le line 59

Source documentation

Concrete polynomial bound on the adaptive coordinate-label count.

theorem selectedAdaptiveMesh_card_le {k q : ℕ} (hk : 3 ≤ k) (hq : 2 ≤ q)
    (hlog : 1 ≤ Real.log k)
    (hqlog : (dimension k : ℝ) * Real.log q ≤
      c * k * Real.log k + dimension k * Real.log (2 * (k : ℝ) ^ 2)) :
    (Fintype.card (selectedAdaptiveMesh hk hq).Label : ℝ) ≤
      28 * (k : ℝ) ^ 3 * Real.log k := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.c, OAI.QuantitativeVanDerWaerden.Parameters.selectedAdaptiveMesh