OAI/Geometry/SurfaceImmersion/Primitive/CenteredAtlasPrimitives.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete finite primitive data from the centered convex phases. The coefficient maps are the actual inverses of their three gradient squares.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.centeredPhaseFamily line 33
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.centeredAtlasBasis line 37
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_centered_atlas_primitives line 48

    Source documentation

    Fixed compact cone and connection data select the phase parameters before the linear perturbations and target. A subordinate circular atlas then gives actual smooth supported amplitudes and an exact global primitive sum.

    theorem compact_centered_atlas_primitives
    (P : A.centers → PhaseBasis)
    (T : A.centers → Set PhaseMean.Tensor)
    (hT : ∀ i, IsCompact (T i))
    (hTpos : ∀ i H, H ∈ T i → ∀ j, 0 < (P i).Q j H)
    (J : A.centers → Set MetricFirstJet)
    (hJ : ∀ i, IsCompact (J i))
    (hdet : ∀ i t, t ∈ J i → metricJetDet t ≠ 0)
    (hw : ∀ i p, 0 ≤ A.weight i p)
    (houter : ∀ i p, p ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 p] (fun _ => 1)) :
    ∃ L r eps : A.centers → ℝ,
      (∀ i, 0 < L i ∧ 0 < r i ∧ 0 < eps i) ∧
…

    Mentions: OAI.ClosedSurfaceR4.PhaseMean.Tensor