OAI/Geometry/SurfaceImmersion/Atlas/WeightedAtlasPhases.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.phaseLinear_smul line 13
2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_smooth line 30
3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_smul_unit line 36
4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_real_smul line 48
5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase_read_derivative_smul_unit line 60

   Source documentation

   Frequency weights scale the read phase derivative everywhere, not just on the compact supports used to establish good geometry.

   lemma linearAtlasPhase_read_derivative_smul_unit (Q : A.centers → PhaseBasis)
       (w : A.centers → Fin 3 → ℝ) (a : A.centers × Fin 3) (k : A.centers)
       (x : SmallModes.Base) :
       phaseDerivative (A.vectorPlaneRead k (A.linearAtlasPhase Q w a)) x =
         w a.1 a.2 •
           phaseDerivative (A.vectorPlaneRead k (A.linearAtlasPhase Q (fun _ _ => 1) a)) x := by
   …

   Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.phaseDerivative