SpatialLoopAmplitude.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

A prescribed spatial amplitude is independent of the varying immersion, even though the coefficient calculus stores it as a function of the full jet.

def OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition line 15
Source documentation
The position slots of an actual low jet.
```
def lowJetPosition : LowJet →L[ℝ] Base :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition_apply line 18
lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition_lowJet line 21
lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition_variationLowJet line 26
def OAI.ClosedSurfaceR4.JetPolynomial.spatialAmplitude line 32
Source documentation
Store a fixed function of position in the existing low-jet coefficient API.
```
def spatialAmplitude (a : Base → ℝ) : LowJet → ℝ := fun J => a (lowJetPosition J)
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.lowJetPosition
lemma OAI.ClosedSurfaceR4.JetPolynomial.spatialAmplitude_smooth line 34
lemma OAI.ClosedSurfaceR4.JetPolynomial.spatialAmplitude_lowJet line 37
lemma OAI.ClosedSurfaceR4.JetPolynomial.spatialAmplitude_variation_zero line 43
Source documentation
The spatial coefficient has zero derivative in every actual map-variation direction: none of the position slots changes with the immersion.
```
lemma spatialAmplitude_variation_zero {a : Base → ℝ} (ha : ContDiff ℝ ∞ a)
    (J : LowJet) (H : Base → Space) (p : Base) :
    fderiv ℝ (spatialAmplitude a) J (variationLowJet H p) = 0 := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.spatialAmplitude, OAI.ClosedSurfaceR4.JetPolynomial.variationLowJet
def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.HasSpatialAmplitude line 60
Source documentation
The given amplitude is fixed as a function of the base point, throughout the whole open jet domain used for nearby immersions.
```
def HasSpatialAmplitude (a : Base → ℝ) : Prop :=
…
```
lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.amplitude_at_lowJet line 63
lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.amplitude_independent_of_map line 71
Source documentation
In particular, changing the immersion does not change the primitive amplitude at the same spatial point.
```
lemma amplitude_independent_of_map {a : Base → ℝ} (ha : l.HasSpatialAmplitude a)
    (G H : JetPolynomial.Base → JetPolynomial.Space) {p : JetPolynomial.Base}
    (hG : lowJet G p ∈ O) (hH : lowJet H p ∈ O) :
    l.amplitude (lowJet G p) = l.amplitude (lowJet H p) :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space
def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.withSpatialAmplitude line 79
Source documentation
Normalize the record field itself to the fixed spatial function while preserving the same velocity loop and its proved geometric identities.
```
def withSpatialAmplitude (a : Base → ℝ) (ha : ContDiff ℝ ∞ a)
    (he : l.HasSpatialAmplitude a) : SurfaceVelocityFamily.Loop O where
…
```
Mentions: OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop
lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.withSpatialAmplitude_amplitude line 97
lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.withSpatialAmplitude_fixed line 101

theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanMetric_eq_spatial_polynomial line 107

Source documentation

The existing mean-polynomial theorem with its primitive rank-one term written as the prescribed spatial amplitude, uniformly for all nearby maps.

theorem meanMetric_eq_spatial_polynomial {a : Base → ℝ} (ha : l.HasSpatialAmplitude a)
    {S : TopologicalSpace.Opens JetPolynomial.Base}
    {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
    (hGO : MapsTo (lowJet G) S O) (n : ℕ) (b c : Bool)
    (U : ℕ → Family S Euclidean)
    (hU : ∀ i, VectorExpression.Represents G (l.coefficientExpressions n i) (U i))
    (z : ℝ) {p : JetPolynomial.Base} (hp : p ∈ S) :
    MetricPolynomial.meanMetric (l.geometry G hG hGO) (coordinateVector 0) U n b c z p =
      inner ℝ
        (fderiv ℝ (fun q => JetVelocityCoordinates.toEuclidean (G q)) p
          (MetricPolynomial.metricDirection (coordinateVector 0) (coordinateVector 1) b))
        (fderiv ℝ (fun q => JetVelocityCoordinates.toEuclidean (G q)) p
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.q, OAI.ClosedSurfaceR4.JetVelocityCoordinates.toEuclidean