DoubleRotationFilling.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit relative filling of the twice-winding planar frame. The third quaternion coordinate is a compact bump; no square-root choice or topological extension assumption is needed.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doubleRotationFrame line 15
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledDoubleRotation line 18
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledDoubleRotation_smooth line 21
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledDoubleRotation_injective line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.filledDoubleRotation_exterior line 52
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_double_rotation_filling line 61
Source documentation
The first column is allowed to move in the interior. On the exterior both columns are exactly those of the squared planar direction.
```
theorem compact_double_rotation_filling {U : Set Base} (hU : IsOpen U) (h0 : 0 ∈ U) :
    ∃ (A : Base → Base →L[ℝ] FrameTarget) (K : Set Base),
      ContDiff ℝ ∞ A ∧ (∀ x, Function.Injective (A x)) ∧ IsCompact K ∧ K ⊆ U ∧
      ∀ x ∉ K, A =ᶠ[𝓝 x] doubleRotationFrame := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.FrameTarget, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doubleRotationFrame