AngularBootstrap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint of the thin-tube bootstrap

This is the order-theoretic step in Proposition prep:thin-upgrade. Its hypotheses describe the closed set of available exponents inside [k - 1, k - 1 / 2], with strict improvement below the endpoint.

theorem OAI.Falconer.thin_tube_bootstrap_endpoint line 21

Source documentation

A closed family of available exponents containing the integer starting exponent and admitting a strict improvement below the desired endpoint contains the half-integer endpoint.

theorem thin_tube_bootstrap_endpoint (k : ℕ) (A : Set ℝ)
    (hclosed : IsClosed A) (hstart : (k : ℝ) - 1 ∈ A)
    (hupper : ∀ q ∈ A, q ≤ (k : ℝ) - 1 / 2)
    (himprove : ∀ q ∈ A, q < (k : ℝ) - 1 / 2 → ∃ q' ∈ A, q < q') :
    (k : ℝ) - 1 / 2 ∈ A := by
…

theorem OAI.Falconer.cap_exponent_loss_transfer line 38
Source documentation
At resolution R⁻¹, increasing the cap exponent by at most e costs only the allowed factor R ^ e. This is the quantitative inequality used when closing the set of available exponents in prep:thin-upgrade.
```
theorem cap_exponent_loss_transfer {R u q q' e : ℝ}
    (hR : 1 ≤ R) (hu : R⁻¹ ≤ u) (hqq : q ≤ q') (hgap : q' - q ≤ e) :
    u ^ q ≤ R ^ e * u ^ q' := by
…
```