LocalAnsatzProfiles.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The leading jets of the supported local ansatz are the geometric profiles of the initial periodic primitive.

def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.globalCoefficients line 23
Source documentation
Retain the actual coefficient values when a supported local family has already been proved smooth after extension by zero.
```
def globalCoefficients (U : ℕ → Family O E)
    (hU : ∀ i, ContDiff ℝ ∞ (fun y : A × ℝ => (U i).val y.1 (y.2 : Period))) :
    ℕ → PeriodicExpansion.Family A E := fun i => ⟨(U i).val,hU i⟩
```
Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.PeriodicExpansion.Family
lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.globalCoefficients_finiteAnsatz line 27
lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.global_angle_eq_local line 33
lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.initial_global_angle line 46
Source documentation
The leading angular correction is the mean-zero velocity primitive.
```
lemma initial_global_angle (W : PeriodicExpansion.Family A E)
    (hW : W.val = g.initial.val) {p : A} (hp : p ∈ O) (t : Period) :
    W.angle.val p t = g.V.val p t-average (g.V.val p) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.initial_global_longitudinal line 54

Source documentation

Adding the leading angular correction to the old longitudinal derivative gives precisely the prescribed velocity profile X.

lemma initial_global_longitudinal {F : A → E} (W : PeriodicExpansion.Family A E)
    (hW : W.val = g.initial.val) (dx : A)
    (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
    {p : A} (hp : p ∈ O) (t : Period) :
    directionalMap F dx p+W.angle.val p t = g.longitudinal.val p t := by
…

Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.initial_global_angle_angle line 67
Source documentation
The second angular derivative of the primitive is the angular derivative of the actual velocity loop, including its normalization by the mean.
```
lemma initial_global_angle_angle (W : PeriodicExpansion.Family A E)
    (hW : W.val = g.initial.val) {p : A} (hp : p ∈ O) (t : Period) :
    W.angle.angle.val p t = g.V.angle.val p t := by
…
```
Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.initial_global_longitudinal_slow line 84

Source documentation

Slow differentiation of the actual leading profile gives X_y, rather than a separately supplied approximation.

lemma initial_global_longitudinal_slow {F : A → E} (hF : ContDiff ℝ ∞ F)
    (W : PeriodicExpansion.Family A E) (hW : W.val = g.initial.val) (dx : A)
    (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
    {p : A} (hp : p ∈ O) (s : ℝ) :
    directionalMap (directionalMap F dx) dy p+
      (W.angle.slow dy).val p (s : Period) =
        (g.longitudinal.slow dy).val p (s : Period) := by
…

Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.compact_initial_ansatz_profiles line 111

Source documentation

All five leading-jet estimates for the same globally smooth local ansatz. The hypotheses are the actual fixed coefficients and their defining primitive identity; no derivative asymptotic is assumed.

theorem compact_initial_ansatz_profiles {F : A → E} (hF : ContDiff ℝ ∞ F)
    (U : ℕ → Family O E)
    (hU : ∀ i, ContDiff ℝ ∞ (fun y : A × ℝ => (U i).val y.1 (y.2 : Period)))
    (hinit : U 0 = g.initial) {Q : Set A} (hQ : IsCompact Q) (hQO : Q ⊆ O)
    (ℓ : A →L[ℝ] ℝ) (dx : A) (hx : ℓ dx = 1) (hy : ℓ dy = 0)
    (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
    (hY : ∀ p ∈ O, fderiv ℝ F p dy = g.Y p) (n : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ z : ℝ, 0 < z → z ≤ 1 → ∀ p ∈ Q,
      let f := finiteAnsatz F U ℓ (n+1) z
…

Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz