PeriodicExpansionStep.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The triangular cancellation step in the finite periodic metric expansion.

structure OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry line 19
Source documentation
The pointwise geometry used by the periodic coefficient recursion.
```
structure Geometry (v : A) where
…
```
def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.longitudinal line 43
def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.transverse line 45
theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.exists_system line 47

theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.exists_cancellation line 82

Source documentation

One new coefficient cancels the current xx and xy fluctuations and the next yy fluctuation, as in the manuscript's triangular recursion.

theorem exists_cancellation (b c d : Family A ℝ) :
    ∃ U : Family A E, (∀ p, average (U.val p) = 0) ∧
      (g.transverse.inner U.angle + b).fluct = 0 ∧
      (g.longitudinal.inner U.angle + c).fluct = 0 ∧
      ((2 : ℝ) • g.transverse.inner (U.slow v) + d).fluct = 0 ∧
      (∀ O : Set A, IsOpen O → (∀ p ∈ O, b.val p = 0) →
        (∀ p ∈ O, c.val p = 0) → (∀ p ∈ O, d.val p = 0) → ∀ p ∈ O, U.val p = 0) := by
…

Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family