InitialAnalyticBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed analytic bounds from a capped initial splitting error

theorem OAI.RegularPointCoordinates.initial_normalizer_norm_sq_le_two line 20

Source documentation

A local volume ratio and the raw initial splitting error bound any chosen exact normalizer on a smaller working set. This applies in particular to the root member of the all-scale normalized family.

theorem initial_normalizer_norm_sq_le_two (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    {p : X} {r ε C : ℝ} {w : X → Euclidean n}
    (hfirst : FirstOrderSplittingOn μ hQ p r ε u w)
    (s : Set X) (hs : MeasurableSet s) (hsub : s ⊆ ball p r)
    (hsne : μ s ≠ 0) (hsfin : μ s ≠ ∞)
    (hrne : μ (ball p r) ≠ 0) (hrfin : μ (ball p r) ≠ ∞)
    (hC : 1 ≤ C) (hε : 0 ≤ ε)
    (hratio : μ.real (ball p r) ≤ C * μ.real s)
    (hsmall : (n : ℝ) ^ 2 * (C * ε) ≤ 1 / 2)
    (A : Euclidean n ≃L[ℝ] Euclidean n)
    (hA : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) s hs A) :
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.splittingDirectionBound_sq_le line 39
Source documentation
Capping the initial error by one gives a fixed all-direction gradient bound, independent of the eventual normalized splitting tolerance.
```
theorem splittingDirectionBound_sq_le {n : ℕ} {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε ≤ 1) :
    ((splittingDirectionBound n ε hε : ℝ≥0) : ℝ) ^ 2 ≤ 4 * (n : ℝ) ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.splittingDirectionBound

theorem OAI.RegularPointCoordinates.initial_working_volume_ratio line 49

Source documentation

The common half-error volume regime bounds the loss from the initial ball to the smaller root ball by a fixed dimensional factor.

theorem initial_working_volume_ratio (μ : Measure X) (n : ℕ) (p q : X)
    {T omega : ℝ} (hT : 0 < T) (homega : 0 < omega)
    (hlarge : |μ.real (ball p (2 * T)) / (omega * (2 * T) ^ n) - 1| ≤ 1 / 2)
    (hsmall : |μ.real (ball q (T / 16)) / (omega * (T / 16) ^ n) - 1| ≤ 1 / 2) :
    μ.real (ball p (2 * T)) ≤ (3 * (32 : ℝ) ^ n) * μ.real (ball q (T / 16)) := by
…