RegularFrameGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual dyadic coordinate frames and their neighboring-ball bounds

def OAI.RegularPointCoordinates.RegularBilinearData.frameAt line 26
Source documentation
Use the same exact dyadic frames already furnished by the construction.
```
def frameAt (q : X) (hq : q ∈ ball base (d.radius / 32)) (i : ℕ) :
    Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.RegularBilinearData.frameAt_exact line 30
theorem OAI.RegularPointCoordinates.RegularBilinearData.frameAt_splitting line 36
theorem OAI.RegularPointCoordinates.RegularBilinearData.frameAt_approximation line 42
theorem OAI.RegularPointCoordinates.RegularBilinearData.mean_upper line 51
Source documentation
Every raw mean energy is bounded by the already constructed common harmonic gradient bound.
```
theorem mean_upper (q : X) (hq : q ∈ ball base (d.radius / 32)) (i : ℕ)
    (v : Euclidean n) :
    ⟪v, sobolevMeanGram (hausdorff n X) hX.quadratic
      (sobolevColumnMap (hausdorff n X) hX.quadratic d.coordinates)
      (ball q (d.radius / 2 ^ i)) measurableSet_ball v⟫_ℝ ≤ (2 * (n : ℝ)) ^ 2 * ‖v‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.sobolevColumnMap
theorem OAI.RegularPointCoordinates.RegularBilinearData.coordinateFrame_lower line 88

theorem OAI.RegularPointCoordinates.regular_subball_mean_comparison line 100

Source documentation

Restricting the actual normalized splitting map to a nearby smaller ball gives a relative bound with just the Euclidean volume-ratio loss.

theorem regular_subball_mean_comparison {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    {q z : X} (hq : q ∈ ball base (e.heat.radius / 32))
    (hz : z ∈ ball base (e.heat.radius / 32)) (hzeta : 0 ≤ zeta)
    (i : ℕ) {theta : ℝ} (htheta : 0 < theta) (htheta1 : theta ≤ 1)
    (hroom : dist z q + theta * (e.heat.radius / 2 ^ i) ≤ e.heat.radius / 2 ^ i)
    (v : Euclidean n) :
    let r := e.heat.radius / (2 : ℝ) ^ i
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.Euclidean