AtlasPrimitiveOperator.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual fiberwise correction operator for independently perturbed primitive cutoffs. Its reference value is the identity, and its inverse solves the finite rank-one equation on the original tensor bundle.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCoefficientField line 38
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitivePhaseCovector line 44
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveFullOperator line 48
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.local_primitive_operator_decomposition line 54

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveFullOperator_reference line 97

Source documentation

At the original square partition the completed operator is exactly the identity, on the full tensor fiber rather than only on a quotient.

theorem primitiveFullOperator_reference
    (P : A.centers → JetPolynomial.Base → PhaseBasis)
    (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))
    (p : M) :
    A.primitiveFullOperator P (fun a => A.weight a.1) (A.curvedAtlasPhase phi) p =
      ContinuousLinearMap.id ℝ (CovariantTwoTensor p) := by
…

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

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveTensor line 130
Source documentation
The corrected tensor is obtained by actual pointwise inverse.
```
def correctedPrimitiveTensor (P : A.centers → JetPolynomial.Base → PhaseBasis)
    (psi : (A.centers × Fin 3) → M → ℝ) (phi : (A.centers × Fin 3) → M → ℝ)
    (u : ∀ p : M, CovariantTwoTensor p) (p : M) : CovariantTwoTensor p :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveTensor_reconstruct line 135

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveTensor_smooth line 153

Source documentation

Smoothness is the ordinary smooth inverse theorem on the tensor bundle.

theorem correctedPrimitiveTensor_smooth
    (P : A.centers → JetPolynomial.Base → PhaseBasis)
    (psi : (A.centers × Fin 3) → M → ℝ) (phi : (A.centers × Fin 3) → M → ℝ)
    (hoperator : ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber →L[ℝ] TensorFiber)) ∞
      (fun p => TotalSpace.mk' (TensorFiber →L[ℝ] TensorFiber) p (A.primitiveFullOperator P psi phi p)))
    (hinv : ∀ p, (A.primitiveFullOperator P psi phi p).IsInvertible)
    (u : ∀ p : M, CovariantTwoTensor p)
    (hu : ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
      (fun p => TotalSpace.mk' TensorFiber p (u p))) :
    ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
      (fun p => TotalSpace.mk' TensorFiber p (A.correctedPrimitiveTensor P psi phi u p)) :=
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveAmplitude line 166
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveAmplitude_square line 172

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveAmplitude_reconstruct line 186

Source documentation

Independent supports retain the exact global rank-one tensor identity.

theorem correctedPrimitiveAmplitude_reconstruct
    (P : A.centers → JetPolynomial.Base → PhaseBasis)
    (psi : (A.centers × Fin 3) → M → ℝ) (phi : (A.centers × Fin 3) → M → ℝ)
    (hinv : ∀ p, (A.primitiveFullOperator P psi phi p).IsInvertible)
    (u : ∀ p : M, CovariantTwoTensor p) (hsymm : ∀ p v w, u p v w = u p w v)
    (hpos : ∀ a p, p ∈ tsupport (psi a) →
      0 ≤ A.primitiveCoefficientField P a p (A.correctedPrimitiveTensor P psi phi u p))
    (p : M) :
    (∑ a : A.centers × Fin 3, (A.correctedPrimitiveAmplitude P psi phi u a p)^2 •
      (A.primitivePhaseCovector phi a p).smulRight (A.primitivePhaseCovector phi a p)) = u p := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveAmplitude_pos_iff line 199
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedPrimitiveAmplitude_smooth line 214