EuclideanHarmonicModel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean harmonic model in the affine-improvement limit

The model retains its actual function, local L² representatives, and normalization. No affine approximation property is included in its data.

theorem OAI.RegularPointCoordinates.euclideanCoordinate_memLp line 20
Source documentation
Each standard coordinate belongs to L² on a finite Euclidean ball.
```
theorem euclideanCoordinate_memLp (n : ℕ) (r : ℝ) (i : Fin n) :
    MemLp (fun z : Euclidean n => z i) 2 (volume.restrict (ball 0 r)) := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.euclideanCoordinateLp line 30
theorem OAI.RegularPointCoordinates.euclideanCoordinateLp_coe line 34
structure OAI.RegularPointCoordinates.EuclideanHarmonicModel line 39
Source documentation
An L²-normalized harmonic function on the limiting Euclidean ball.
```
structure EuclideanHarmonicModel (n : ℕ) (S : ℝ) where
…
```
def OAI.RegularPointCoordinates.EuclideanHarmonicModel.localLp line 46
theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.localLp_coe line 51
def OAI.RegularPointCoordinates.EuclideanHarmonicModel.moments line 57
Source documentation
Target, constant and identity coordinates, all in the normalized local L² space. Their finite moments are the compactness output needed.
```
def EuclideanHarmonicModel.moments {n : ℕ} {S r : ℝ}
    (w : EuclideanHarmonicModel n S) (hr : r ≤ S) :
    Option (Option (Fin n)) → Lp ℝ 2 (volume.restrict (ball (0 : Euclidean n) r)) :=
…
```
Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput line 70
Source documentation
Evans, PDE (second edition), §2.2.3(c), Theorem 7, degree two, combined with Cauchy--Schwarz on the outer ball. The input only bounds the second derivative of a normalized Euclidean harmonic function.
```
def EuclideanHarmonicHessianInput (n : ℕ) : Prop :=
…
```