OAI/Geometry/RCD/Sobolev/InnerProductVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a varying pairing from its frozen pairing

Only continuity of the second vector is needed once its pairing against the fixed first vector has a scalar derivative.

  1. theorem OAI.RegularPointCoordinates.hasDerivAt_inner_of_frozen line 22

    Source documentation

    A scalar product rule that does not ask the second vector for a vector-valued derivative.

    theorem hasDerivAt_inner_of_frozen {W Q : ℝ → E} {t : ℝ} {W' : E} {a : ℝ}
    (hW : HasDerivAt W W' t) (hQ : ContinuousAt Q t)
    (hfixed : HasDerivAt (fun s => inner ℝ (W t) (Q s)) a t) :
    HasDerivAt (fun s => inner ℝ (W s) (Q s)) (inner ℝ W' (Q t)+a) t := by
…