OAI/Geometry/SurfaceImmersion/Primitive/CurvedAtlasPrimitives.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Positive primitive amplitudes for point-dependent phase bases. The basis can be the actual nonlinear gradient basis constructed in SpatialPhaseBasis; no constant-phase restriction enters the algebra.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPhaseCoefficient line 36
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPhaseTensor line 39
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude line 42
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveTensor line 46
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude_support line 51
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude_nonneg line 55
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude_pos_iff line 60
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude_square line 71
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.sum_curvedPhaseTensor line 85
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restored_curvedPrimitiveTensor line 97
  11. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.sum_curvedPrimitiveTensor line 112

    Source documentation

    The actual curved-basis amplitudes give an exact finite decomposition.

    theorem sum_curvedPrimitiveTensor (hu : ∀ p v w, u p v w = u p w v)
    (hpos : ∀ i j p, p ∈ tsupport (A.weight i) →
      0 ≤ (P i (chart (i : M) p)).Q j (A.tensorChartRead i u (chart (i : M) p))) (p : M) :
    ∑ a : A.centers × Fin 3, A.curvedPrimitiveTensor P u a p = u p := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart

  12. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedAtlasPhase line 126
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedAtlasPhase_smooth line 130
  14. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedAtlasPhase_eventually line 136
  15. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedAtlasPhase_mfderiv line 146
  16. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveTensor_apply line 170

    Source documentation

    Every restored tensor is the actual square of its global phase covector wherever its amplitude is supported.

    lemma curvedPrimitiveTensor_apply
    (phi : A.centers → Fin 3 → SmallModes.Base → ℝ)
    (hphi : ∀ i j, ContDiff ℝ ∞ (phi i j))
    (houter : ∀ i p, p ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 p] (fun _ => 1))
    (hfit : ∀ i j p, p ∈ tsupport (A.weight i) →
      (P i (chart (i : M) p)).ξ j = phaseDerivative (phi i j) (coordinateChart (i : M) p))
    (a : A.centers × Fin 3) (p : M) (v w : TangentSpace planeModel p) :
    A.curvedPrimitiveTensor P u a p v w =
      (A.curvedPrimitiveAmplitude P u a p)^2 *
        (show ℝ from mfderiv planeModel 𝓘(ℝ) (A.curvedAtlasPhase phi a) p v) *
        (show ℝ from mfderiv planeModel 𝓘(ℝ) (A.curvedAtlasPhase phi a) p w) := by
…

    Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.phaseDerivative, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.planeModel

  17. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.curvedPrimitiveAmplitude_smooth line 207