ManifoldFreeIncrement.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Local free oscillations as maps on the surface

The finite-mode construction takes place in coordinates. These lemmas extend its supported output by zero on the surface, preserving smoothness and support. This is the first globalization step for the small increments.

theorem OAI.ClosedSurfaceR4.contMDiff_indicator_of_support line 25

Source documentation

Extension by zero across a closed support lying inside the smooth chart.

theorem contMDiff_indicator_of_support {V : Type*} [NormedAddCommGroup V]
    [NormedSpace ℝ V] {O S : Set M} {Z : M → V}
    (hO : IsOpen O) (hS : IsClosed S) (hSO : S ⊆ O)
    (hZ : ContMDiffOn planeModel 𝓘(ℝ, V) ∞ Z O)
    (hz : ∀ x ∈ O, x ∉ S → Z x = 0) :
    ContMDiff planeModel 𝓘(ℝ, V) ∞ (O.indicator Z) ∧
      tsupport (O.indicator Z) ⊆ S := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel

structure OAI.ClosedSurfaceR4.ManifoldFreeChart line 48
Source documentation
Coordinate data for one supported free mode. The representative model is a genuine smooth extension of the immersed map in these coordinates.
```
structure ManifoldFreeChart (F : M → Space) (S : Set M) where
…
```
Mentions: OAI.ClosedSurfaceR4.Space
def OAI.ClosedSurfaceR4.ManifoldFreeChart.increment line 67
Source documentation
The oscillatory increment, written directly as an ambient four-space map.
```
def increment (c : ManifoldFreeChart F S) (ψ u : SmallModes.Base → ℝ)
    (δ τ : ℝ) (q : ℕ) : M → Space :=
…
```
Mentions: OAI.ClosedSurfaceR4.ManifoldFreeChart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.Space

theorem OAI.ClosedSurfaceR4.ManifoldFreeChart.increment_smooth_support line 75

Source documentation

The local finite free mode extends smoothly by zero on the manifold. No regularity of its values outside the coordinate source is required.

theorem increment_smooth_support (c : ManifoldFreeChart F S)
    {ψ u : SmallModes.Base → ℝ}
    (hb : ContDiffOn ℝ ∞ (phaseAmplitude ψ u) c.target)
    (hsp : ∀ x ∈ c.source, c.coord x ∈ tsupport ψ → x ∈ S)
    (δ τ : ℝ) (q : ℕ) :
    ContMDiff planeModel spaceModel ∞ (c.increment ψ u δ τ q) ∧
      tsupport (c.increment ψ u δ τ q) ⊆ S := by
…

Mentions: OAI.ClosedSurfaceR4.ManifoldFreeChart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.planeModel

theorem OAI.ClosedSurfaceR4.ManifoldFreeChart.increment_eq_on_source line 104

Source documentation

On the source chart the global increment is the original finite mode.

theorem increment_eq_on_source (c : ManifoldFreeChart F S)
    (ψ u : SmallModes.Base → ℝ) (δ τ : ℝ) (q : ℕ)
    {x : M} (hx : x ∈ c.source) :
    spaceCoordinates (c.increment ψ u δ τ q x) =
      realOsc τ (modeApprox τ (fun y => complexify (c.model y))
        (freeSeed δ τ (phaseAmplitude ψ u) c.model) (fun _ => 0) q) (c.coord x) := by
…

Mentions: OAI.ClosedSurfaceR4.ManifoldFreeChart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates

theorem OAI.ClosedSurfaceR4.ManifoldFreeChart.increment_hasCompactSupport line 112

theorem OAI.ClosedSurfaceR4.finite_free_increment_smooth_support line 123

Source documentation

Finitely many coordinate free modes give one smooth ambient correction, supported in the union of their prescribed supports.

theorem finite_free_increment_smooth_support {ι : Type*} [Fintype ι]
    {F : M → Space} {S : ι → Set M} (c : ∀ i, ManifoldFreeChart F (S i))
    (ψ u : ι → SmallModes.Base → ℝ)
    (hb : ∀ i, ContDiffOn ℝ ∞ (phaseAmplitude (ψ i) (u i)) (c i).target)
    (hsp : ∀ i x, x ∈ (c i).source → (c i).coord x ∈ tsupport (ψ i) → x ∈ S i)
    (δ τ : ℝ) (q : ℕ) :
    ContMDiff planeModel spaceModel ∞ (fun x => ∑ i, (c i).increment (ψ i) (u i) δ τ q x) ∧
      tsupport (fun x => ∑ i, (c i).increment (ψ i) (u i) δ τ q x) ⊆ ⋃ i, S i := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.ManifoldFreeChart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.planeModel