OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/DirectionalFourthDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fourth derivatives along the affine coordinate lines used by cubature.

  1. theorem OAI.ContinuumCoulomb.fourthDeriv_affine_line line 12

    Source documentation

    Local smoothness suffices; the function may be singular away from the line point.

    theorem fourthDeriv_affine_line (f : Position → ℝ) (b v : Position) (t : ℝ)
    (hf : ContDiffAt ℝ 4 f (b+t • v)) :
    iteratedDeriv 4 (fun s : ℝ => f (b+s • v)) t =
      iteratedFDeriv ℝ 4 f (b+t • v) (fun _ => v) := by
…

    Mentions: OAI.ContinuumCoulomb.Position

  2. theorem OAI.ContinuumCoulomb.fourthDeriv_affine_line_bound line 36