PositiveDensityTurns.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive changes of circle coordinate preserve stationary points and their spatial jets.

lemma OAI.ClosedSurfaceR4.PositiveDensity.hasDerivAt_inverseClock line 15
lemma OAI.ClosedSurfaceR4.PositiveDensity.deriv_reparametrize_eq_zero_iff line 34

theorem OAI.ClosedSurfaceR4.PositiveDensity.spatial_derivative_at_turn line 53

Source documentation

At a turn, the extra spatial chain-rule term from the inverse clock is zero.

theorem spatial_derivative_at_turn
    (hU : IsOpen U) (hρ : ContDiffOn ℝ ∞ ρ (U ×ˢ univ))
    (hpos : ∀ b ∈ U, ∀ t, 0 < ρ (b, t))
    (hper : ∀ b ∈ U, Function.Periodic (fun t => ρ (b, t)) 1)
    (hmass : ∀ b ∈ U, (∫ t in 0..1, ρ (b, t)) = 1)
    {F : B × ℝ → E} (hF : ContDiffOn ℝ ∞ F (U ×ˢ univ))
    {b : B} (hb : b ∈ U) (θ : ℝ)
    (hzero : fderiv ℝ F (b, inverseClock ρ b θ) (0, 1) = 0) (v : B) :
    fderiv ℝ (fun x => reparametrize ρ F (x, θ)) b v =
      fderiv ℝ (fun x => F (x, inverseClock ρ b θ)) b v := by
…

Mentions: OAI.ClosedSurfaceR4.PositiveDensity.inverseClock, OAI.ClosedSurfaceR4.PositiveDensity.reparametrize