TensorRootPhases.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual cutoff square-root amplitudes for global symmetric tensors. Their squared phase tensors give the exact global atlas decomposition.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.rootPhaseAmplitude line 29
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.rootPhaseAmplitude_support line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.rootPhaseAmplitude_smooth line 39
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.rootPhaseAmplitude_square line 56
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restored_rootPhase line 73

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.global_rootPhase_decomposition line 92

Source documentation

No positive-definiteness assumption is hidden here: only the explicitly listed phase coefficients must be nonnegative on their supports.

theorem global_rootPhase_decomposition (P : A.centers → PhaseBasis) (w : A.centers → Fin 3 → ℝ)
    (u : ∀ x : M, CovariantTwoTensor x) (hu : ∀ p v v', u p v v' = u p v' v)
    (hw : ∀ i j, w i j ≠ 0)
    (hpos : ∀ i j p, p ∈ tsupport (A.weight i) →
      0 ≤ (P i).Q j (A.tensorChartRead i u (chart (i : M) p))) (p : M) :
    (∑ i : A.centers, ∑ j : Fin 3,
      ((A.rootPhaseAmplitude i ((P i).Q j) (w i j) u p)^2 * (w i j)^2) •
        A.bundleRestore A.tensorTriv i (fun _ => fiberFromThree (covectorSquare ((P i).ξ j))) p) =
      u p := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree