OAI/Geometry/SurfaceImmersion/Primitive/PeriodicCoefficientProfiles.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite coefficient bounds for the varying-map version of the periodic derivative estimates.

  1. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.phaseSum_bound_of_coefficients line 16
  2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.phaseSum_tail_bound_of_coefficients line 32
  3. theorem OAI.ClosedSurfaceR4.PeriodicExpansion.transverse_profiles_of_coefficients line 43

    Source documentation

    The two transverse derivatives only differentiate slow coefficients.

    theorem transverse_profiles_of_coefficients {F : A → E} (hF : ContDiff ℝ ∞ F)
    (U : ℕ → Family A E) (ℓ : A →L[ℝ] ℝ) (L : ℕ) {dy : A} (hy : ℓ dy = 0)
    {z C : ℝ} {p : A} (hz : 0 < z) (hz1 : z ≤ 1) (hC : 0 ≤ C)
    (hU : ∀ i < L, ‖((U i).slow dy).fastValue ℓ z p‖ ≤ C)
    (hUU : ∀ i < L, ‖(((U i).slow dy).slow dy).fastValue ℓ z p‖ ≤ C) :
    ‖directionalMap (finiteAnsatz F U ℓ L z) dy p-directionalMap F dy p‖ ≤ (L*C)*z ∧
    ‖directionalMap (directionalMap (finiteAnsatz F U ℓ L z) dy) dy p-
      directionalMap (directionalMap F dy) dy p‖ ≤ (L*C)*z := by
…

    Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family, OAI.ClosedSurfaceR4.PeriodicExpansion.directionalMap, OAI.ClosedSurfaceR4.PeriodicExpansion.finiteAnsatz

  4. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.global_slow_eq_local line 69
  5. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.global_slow_eq_local_of_eqOn line 76