Calculus along affine segments

The derivative and fundamental theorem of calculus along t ↦ x + t • v, at C¹ regularity on an arbitrary real normed vector space. Translation estimates, difference quotients and ray-integral arguments share these identities.

theorem EllipticPdes.Analysis.hasDerivAt_comp_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : Differentiable ℝ f) (x v : E) (t : ℝ) : HasDerivAt (fun (s : ℝ) => f (x + s • v)) ((fderiv ℝ f (x + t • v)) v) t

The derivative of a differentiable function along an affine segment.

theorem EllipticPdes.Analysis.continuous_segment_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x v : E) : Continuous fun (t : ℝ) => (fderiv ℝ f (x + t • v)) v

The directional derivative of a C¹ function is continuous along a segment.

theorem EllipticPdes.Analysis.continuous_squared_segment_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (v : E) : Continuous (Function.uncurry fun (x : E) (t : ℝ) => (fderiv ℝ f (x + t • v)) v ^ 2)

Joint continuity of the squared directional derivative along a segment.

theorem EllipticPdes.Analysis.sub_translation_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x v : E) : f (x + v) - f x = ∫ (t : ℝ) in 0..1, (fderiv ℝ f (x + t • v)) v

Fundamental theorem of calculus along the segment from x to x + v.

theorem EllipticPdes.Analysis.sq_sub_translation_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x v : E) : (f (x + v) - f x) ^ 2 ≤ ∫ (t : ℝ) in 0..1, (fderiv ℝ f (x + t • v)) v ^ 2

The squared increment is bounded by the integral of the squared segment derivative.