OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicExpansionStep.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite periodic cancellation step on an open admissible domain.

  1. structure OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry line 17
  2. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.longitudinal line 40
  3. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.transverse line 42
  4. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.exists_system line 44
  5. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.exists_cancellation line 99

    Source documentation

    One coefficient cancels the next three fluctuation equations.

    theorem exists_cancellation (b c d : Family O ℝ) :
    ∃ U : Family O E, (∀ p ∈ O, 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 ∧
      (∀ Z : Set A, IsOpen Z → Z ⊆ O → (∀ p ∈ Z, b.val p = 0) →
        (∀ p ∈ Z, c.val p = 0) → (∀ p ∈ Z, d.val p = 0) → ∀ p ∈ Z, U.val p = 0) := by
…

    Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family