PPTGridCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting the finite paired-grid labels at a local PPT comparison scale. The bound uses the local dimension and the actual mesh, independently of the ambient Ford bands or a globally chosen normality cutoff.

lemma OAI.TotientAsymptotic.ppt_mesh_reciprocal_lower line 18
Source documentation
The actual PPT mesh is at least the reciprocal of its local double logarithm. Doubling this mesh preserves the same lower bound.
```
lemma ppt_mesh_reciprocal_lower {t : ℝ} (ht0 : 0 < t) (ht : 1 ≤ Real.log t) :
    1/t ≤ (Real.log t)^5/Real.sqrt t := by
…
```
theorem OAI.TotientAsymptotic.ppt_grid_card_bound line 32
Source documentation
There are at most exponentially many grid labels in the square of the logarithm of the local double-logarithmic scale.
```
theorem ppt_grid_card_bound {A t δ : ℝ} {b : ℕ}
    (ht0 : 0 < t) (ht : 1 ≤ Real.log t) (hδ : 0 < δ) (hmesh : 1/t ≤ δ)
    (hdim : (b : ℝ) ≤ A*Real.log t) :
    ((collisionGridFamilies δ b).card : ℝ) ≤
      Real.exp (2*A*(Real.log t)^2) := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.collisionGridFamilies

theorem OAI.TotientAsymptotic.ppt_grid_and_subsets_card_bound line 66

Source documentation

Removing arbitrary matched coordinates costs at most another exponential-square factor; every subset is counted.

theorem ppt_grid_and_subsets_card_bound {A t δ : ℝ} {b H : ℕ}
    (ht0 : 0 < t) (ht : 1 ≤ Real.log t) (hδ : 0 < δ) (hmesh : 1/t ≤ δ)
    (hb : (b : ℝ) ≤ A*Real.log t) (hH : (H : ℝ) ≤ A*Real.log t) :
    ((collisionGridFamilies δ b).card : ℝ)*
        (((Finset.range H).powerset).card : ℝ) ≤
      Real.exp (3*A*(Real.log t)^2) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.collisionGridFamilies