OAI/Geometry/SurfaceImmersion/Primitive/PeriodicSubspace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit covariance and primitive operations preserve a fixed subspace at each parameter value; no choice of a moving frame is required.

  1. lemma OAI.ClosedSurfaceR4.CovarianceCorrector.average_mem_submodule line 17
  2. lemma OAI.ClosedSurfaceR4.CovarianceCorrector.covariance_mem_submodule line 22
  3. lemma OAI.ClosedSurfaceR4.CovarianceCorrector.covarianceSolution_mem_submodule line 32

    Source documentation

    The equation for m forces m into the velocity plane, since both terms on its right side belong to that plane.

    lemma covarianceSolution_mem_submodule (P : Submodule ℝ E)
    (V : C(Period, E)) (r : C(Period, ℝ)) (hmem : ∀ t, V t ∈ P)
    {q : ℝ} (hq : 0 < q) (hcircle : ∀ t, inner ℝ (V t) (V t) = q) :
    covarianceSolution V r q ∈ P := by
…

    Mentions: OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.CovarianceCorrector.covarianceSolution

  4. lemma OAI.ClosedSurfaceR4.CovarianceCorrector.parameterCorrector_mem_submodule line 46
  5. lemma OAI.ClosedSurfaceR4.PeriodicPrimitive.intervalIntegral_mem_submodule line 63
  6. lemma OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_mem_submodule line 72