PoissonSpan.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual span of harmonic coordinates and two Poisson replacements

def OAI.RegularPointCoordinates.poissonSpan line 21
Source documentation
The last two components are the Poisson replacements used in a same-scale two-center comparison.
```
def poissonSpan {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (f : Fin 2 → SobolevSpace μ hQ) : Fin (n + 2) → SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
def OAI.RegularPointCoordinates.poissonSpanLaplacian line 27
Source documentation
Both replacements have the same constant Laplacian; the harmonic coordinate components have zero Laplacian.
```
def poissonSpanLaplacian (n : ℕ) (c : ℝ) : Euclidean (n + 2) →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.poissonSpan_constant_laplacian line 32

theorem OAI.RegularPointCoordinates.poissonSpan_gradient line 57

Source documentation

Component estimates give the full directional gradient estimate required by the single shared Bochner measure.

theorem poissonSpan_gradient {n : ℕ} {Ω : Set X}
    (u : Fin n → SobolevSpace μ hQ) (f : Fin 2 → SobolevSpace μ hQ) (B : ℝ)
    (hu : ∀ i, ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ (u i) (u i) x ≤ B ^ 2)
    (hf : ∀ i, ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ (f i) (f i) x ≤ B ^ 2)
    (v : Euclidean (n + 2)) :
    ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ
      (sobolevColumnMap μ hQ (poissonSpan μ hQ u f) v)
      (sobolevColumnMap μ hQ (poissonSpan μ hQ u f) v) x ≤
        (((n + 2 : ℕ) : ℝ) * B) ^ 2 * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.poissonSpan

theorem OAI.RegularPointCoordinates.local_poisson_span line 77

Source documentation

The local estimates now produce the shared Bochner measure for the actual coordinates and replacements. The height hypotheses are exactly the output of the positive-source Poisson estimates.

theorem local_poisson_span {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (hn : 2 ≤ n) (hgradient : LocalPoissonGradientInput hX)
    (hhessian : LocalPoissonHessianInput hX)
    {κ r ε H c Bq : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (p : X) (hr : 0 < r) (hcurv : -1 ≤ K * (2 * r) ^ 2)
    (hε : 0 ≤ ε) (hH : 0 ≤ H) (hBqH : Bq ≤ H)
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (f q : Fin 2 → SobolevSpace (hausdorff n X) hX.quadratic)
    (hu : ∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p (8 * r)) (u i))
    (hgrad : ∀ i, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8 * r)),
      localGamma (hausdorff n X) hX.quadratic (u i) (u i) x ≤ (1 + ε) ^ 2)
    (hf : ∀ i, IsConstantLaplacianOn (hausdorff n X) hX.quadratic
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonGradientInput, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.IsConstantLaplacianOn