PrimitiveFiberInverse.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The finite rank-one correction acts on symmetric tensors. Adding the identity on the antisymmetric summand gives an honest invertible operator on the full four-dimensional tensor fiber, without an orientation choice.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorSymmetrizer line 24
Source documentation
Intrinsic symmetrization of a bilinear form.
```
def tensorSymmetrizer : TensorFiber →L[ℝ] TensorFiber :=
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorSymmetrizer_apply line 28
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorSymmetrizer_symmetric line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorSymmetrizer_eq_self line 37
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorSymmetrizer_idempotent line 43
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator line 50
Source documentation
The actual finite supported primitive operator, in one fiber.
```
def finitePrimitiveOperator (q : ι → TensorFiber →L[ℝ] ℝ)
    (psi : ι → ℝ) (xi : ι → Plane →L[ℝ] ℝ) : TensorFiber →L[ℝ] TensorFiber :=
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.Plane
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator_apply line 54
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator_symmetric line 61
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator_symmetrizer line 70
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator line 75
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator_apply line 79
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator_eq_id line 84
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator_inverse_symmetric line 98
Source documentation
The inverse of the completed operator solves precisely the original symmetric rank-one equation; the auxiliary antisymmetric identity vanishes.
```
theorem completedPrimitiveOperator_inverse_symmetric
    (q : ι → TensorFiber →L[ℝ] ℝ) (psi : ι → ℝ) (xi : ι → Plane →L[ℝ] ℝ)
    (hinv : (completedPrimitiveOperator q psi xi).IsInvertible)
    {H : TensorFiber} (hH : ∀ v w, H v w = H w v) :
    let B := (completedPrimitiveOperator q psi xi).inverse H
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator
abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveFiberParameters line 121
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator_smooth line 123

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_positive_primitive_inverse line 140

Source documentation

Invertibility and positivity are obtained on an actual open neighborhood of the reference cutoff/covector data, uniformly for a compact target set.

theorem compact_positive_primitive_inverse
    (q : ι → TensorFiber →L[ℝ] ℝ) (psi₀ : ι → ℝ) (xi₀ : ι → Plane →L[ℝ] ℝ)
    (hbase : ∀ B : TensorFiber, (∀ v w, B v w = B w v) →
      finitePrimitiveOperator q psi₀ xi₀ B = B)
    {K : Set TensorFiber} (hK : IsCompact K)
    (hpos : ∀ H ∈ K, ∀ i, 0 < q i H) :
    ∃ eps : ℝ, 0 < eps ∧ ∀ z : PrimitiveFiberParameters ι,
      ‖z-(psi₀,xi₀)‖ < eps →
      (completedPrimitiveOperator q z.1 z.2).IsInvertible ∧
        ∀ H ∈ K, ∀ i, 0 < q i ((completedPrimitiveOperator q z.1 z.2).inverse H) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finitePrimitiveOperator, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveFiberParameters, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.completedPrimitiveOperator