Increments along a quarter rotation

For (x, y) ∈ E × E and the rotation R θ (x, y) = (cos θ • x + sin θ • y, -sin θ • x + cos θ • y) (ContinuousLinearMap.rotation), the first coordinate of R θ (x, y) runs along a quarter circle from x (at θ = 0) to y (at θ = π / 2) with velocity the second coordinate. By the fundamental theorem of calculus, the increment of a C¹ function f between x and y is

f y - f x = ∫ θ in 0..π/2, f' (R θ (x, y)).1 (R θ (x, y)).2.

This is the interpolation identity behind the Maurey–Pisier proof of Gaussian concentration.

Main results

• ContDiff.sub_eq_integral_fderiv_rotation: the identity above.

theorem ContDiff.sub_eq_integral_fderiv_rotation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ 1 f) (p : E × E) : f p.2 - f p.1 = ∫ (θ : ℝ) in 0..Real.pi / 2, (fderiv ℝ f ((ContinuousLinearMap.rotation θ) p).1) ((ContinuousLinearMap.rotation θ) p).2

The Gaussian interpolation identity. The first coordinate of the rotation of (x, y) by θ runs from x (at θ = 0) to y (at θ = π / 2) with velocity the second coordinate, so the increment of a C¹ function between x and y is the integral of its derivative along this quarter circle.