PhasePrimitiveBoundaryGauss.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A tensor restored in a chart reads back exactly where its outer cutoff is one.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseMetricRead_primitive_germ line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_primitive_gauss_zero line 49

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_primitive_boundary_crossing line 78

Source documentation

At a zero of the amplitude, the original immersion's ordered crossing invariant is exactly the scalar boundary expression for the new metric.

lemma phase_primitive_boundary_crossing (i : A.centers)
    (e : OpenPartialHomeomorph Base Base) (he : ContDiff ℝ ∞ e) (hi : ContDiff ℝ ∞ e.symm)
    {g : SmoothMetric M} {F : M → Space} (hF : IsSmoothIsometricImmersion M g F)
    (h : SmoothMetric M) {χ : Base → ℝ} (hχ : ContDiff ℝ ∞ χ)
    {a : SmallModes.Base → ℝ} (ha : ContDiff ℝ ∞ a)
    (htarget : h.inner = g.inner + A.bundleRestore A.tensorTriv i
      (fun y => fiberFromThree (localizedTensorPullback e χ (fun q => ![(a (baseEquiv q))^2,0,0]) y)))
    {x : SmallModes.Base} (hx : baseEquiv.symm x ∈ e.target)
    (hactive : A.chartWeight i (e.symm (baseEquiv.symm x)) ≠ 0)
    (hz : a x = 0) (hnonneg : ∀ᶠ y in 𝓝 x, 0 ≤ a y)
    (hD : NormalFrame.gramDet
      (SmallModes.coordDeriv SmallModes.dx (A.phaseRealChartMap i e.symm F) x)
…

Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree, OAI.ClosedSurfaceR4.NormalFrame.gramDet, OAI.ClosedSurfaceR4.SmallModes.coordDeriv, OAI.ClosedSurfaceR4.SmallModes.dx