OAI/Geometry/SurfaceImmersion/Primitive/SlowPeriodicDerivative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Slow differentiation commutes with the periodic mean.

  1. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.slowDerivative line 17
  2. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.contDiff_slowDerivative line 20
  3. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.fderiv_slice line 24
  4. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.periodic_slowDerivative line 29
  5. def OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.slowDerivativeFamily line 37
  6. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.slowDerivativeFamily_smooth line 43
  7. lemma OAI.ClosedSurfaceR4.SmoothPeriodicCalculus.slowDerivativeFamily_mean_zero line 50
  8. theorem OAI.ClosedSurfaceR4.PeriodicCorrector.directional_pairing_constraint line 80

    Source documentation

    The differentiated pairing constraint in an arbitrary slow direction.

    theorem directional_pairing_constraint {Y U : A → E} {H : A → ℝ}
    {p v : A} {C : E} {j : ℝ}
    (hY : DifferentiableAt ℝ Y p) (hU : DifferentiableAt ℝ U p)
    (hH : DifferentiableAt ℝ H p) (he : ∀ q, inner ℝ (Y q) (U q) = H q)
    (hC : fderiv ℝ Y p v = C)
    (hK : inner ℝ C (U p) = fderiv ℝ H p v - j) :
    inner ℝ (Y p) (fderiv ℝ U p v) = j := by
…