ChartJetOperators.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual stationary operators on a smooth pole patch

The operators are the quadratic Laplacian jets of the explicit chart amplitude. They depend smoothly on the evaluation direction away from the opposite pole. Their equality with the coefficients in the local sphere expansion follows by locality, including the fixed chart cutoff.

def OAI.Falconer.unmaskedStationaryAmplitude line 21
theorem OAI.Falconer.unmaskedStationaryAmplitude_contDiffAt line 26
def OAI.Falconer.actualStationaryCoefficient line 45
theorem OAI.Falconer.actualStationaryCoefficient_contDiffAt line 49
theorem OAI.Falconer.actualStationaryCoefficient_eq line 56
theorem OAI.Falconer.actualStationaryCoefficient_zero line 70
theorem OAI.Falconer.actualStationaryCoefficient_local line 79
Source documentation
The actual coefficient depends only on the original amplitude near its evaluation direction; every cutoff that is constant there is invisible.
```
theorem actualStationaryCoefficient_local (m j : ℕ) {B G : Space (m+3) → ℂ}
    (e : Sphere (m+3)) (hBG : B =ᶠ[𝓝 (e : Space (m+3))] G) :
    actualStationaryCoefficient m j B e = actualStationaryCoefficient m j G e := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.actualStationaryCoefficient