AtlasTensorTransition.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual change of tensor coordinates for a restored atlas term. Bundle restoration uses one outer cutoff, whereas chart reading uses the square of its own cutoff. On the nonzero partition locus the latter is one.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_bundleRestore_transition line 39
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_bundleRestore_of_weight_ne_zero line 56
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_bundleRestore_eventually line 67
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorRestoreTransition line 83
Source documentation
The three-coordinate form of the genuine tensor-bundle transition, including the single cutoff used by restoration.
```
def tensorRestoreTransition (i j : A.centers) (x : Base) : Tensor →L[ℝ] Tensor :=
…
```
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorRestoreTransition_smoothOn line 87
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_restoreThree line 100
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weighted_tensorChartRead_restoreThree line 109

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_tensorRestoreTransition line 123

Source documentation

The finite-dimensional tensor transition extends smoothly off any compact overlap. The extension is independent of the restored field.

theorem compact_tensorRestoreTransition (i j : A.centers) {K : Set Base}
    (hK : IsCompact K) (hKe : K ⊆ (transition (i : M) (j : M)).source) :
    ∃ U : Set Base, IsOpen U ∧ K ⊆ U ∧
      U ⊆ (transition (i : M) (j : M)).source ∧
      ∃ L : Base → Tensor →L[ℝ] Tensor, ContDiff ℝ ∞ L ∧
        EqOn L (A.tensorRestoreTransition i j) U ∧
        (∀ (f : Base → Tensor) (x : Base), x ∈ U →
          (A.weight i ((chart (i : M)).symm x)) ^ 2 •
              A.tensorChartRead i
                (A.bundleRestore A.tensorTriv j (fun y => fiberFromThree (f y))) x =
            (A.weight i ((chart (i : M)).symm x)) ^ 2 •
              L x (f (transition (i : M) (j : M) x))) := by
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pair_tensorRestoreTransition line 145