SphereIntegration.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.sphereIsometry line 17
Source comment
The action of a genuine orthogonal coordinate change on the unit sphere.
```
def sphereIsometry (A : E ≃ₗᵢ[ℝ] E) : sphere (0 : E) 1 ≃ₜ sphere (0 : E) 1 :=
…
```
theorem OAI.AffineBernstein.sphereIsometry_coe line 20
theorem OAI.AffineBernstein.sphereIsometry_measurePreserving line 30
Source comment
The round measure, defined by ordinary Euclidean polar coordinates, is orthogonally invariant in every dimension, including the two-point sphere.
```
theorem sphereIsometry_measurePreserving (A : E ≃ₗᵢ[ℝ] E) :
    MeasurePreserving (sphereIsometry A) volume.toSphere volume.toSphere := by
…
```
Mentions: OAI.AffineBernstein.sphereIsometry
theorem OAI.AffineBernstein.integral_sphere_isometry line 56
def OAI.AffineBernstein.rotationGenerator line 64
Source comment
The infinitesimal generator of rotation in the oriented `u,v` plane.
```
def rotationGenerator (u v : E) : E →L[ℝ] E :=
…
```
def OAI.AffineBernstein.planeProjection line 68
def OAI.AffineBernstein.planeRotationMap line 72
theorem OAI.AffineBernstein.planeRotationMap_apply line 76
theorem OAI.AffineBernstein.planeRotationMap_inner line 85
def OAI.AffineBernstein.planeRotation line 98
Source comment
A genuine orthogonal rotation; its formula is the usual two-plane rotation, not an assumed measure-invariant flow.
```
def planeRotation {u v : E} (hu : inner ℝ u u = 1)
    (hv : inner ℝ v v = 1) (huv : inner ℝ u v = 0) (t : ℝ) : E ≃ₗᵢ[ℝ] E :=
…
```
theorem OAI.AffineBernstein.planeRotation_apply line 106
theorem OAI.AffineBernstein.planeRotation_zero line 110
theorem OAI.AffineBernstein.planeRotation_hasDerivAt line 113
theorem OAI.AffineBernstein.planeRotation_continuous line 123
theorem OAI.AffineBernstein.planeRotation_mem_sphere line 128
theorem OAI.AffineBernstein.planeRotation_sphere_continuous line 137

theorem OAI.AffineBernstein.hasDerivAt_integral_compact line 144

Source comment

Differentiation under a finite measure on a compact parameter space. The uniform bound is proved, rather than supplied as an analytic assumption.

theorem hasDerivAt_integral_compact {α : Type*} [TopologicalSpace α] [CompactSpace α]
    [MeasurableSpace α] [BorelSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    {F D : ℝ → α → ℝ}
    (hF : Continuous (fun p : ℝ × α => F p.1 p.2))
    (hD : Continuous (fun p : ℝ × α => D p.1 p.2))
    (hd : ∀ t a, HasDerivAt (fun r => F r a) (D t a) t) :
    HasDerivAt (fun t => ∫ a, F t a ∂μ) (∫ a, D 0 a ∂μ) 0 := by
…

theorem OAI.AffineBernstein.integral_sphere_rotation_deriv line 169

Source comment

Infinitesimal orthogonal invariance of the actual round measure. This is proved by differentiating the genuine rotation, with a compact-sphere bound.

theorem integral_sphere_rotation_deriv {u v : E} (hu : inner ℝ u u = 1)
    (hv : inner ℝ v v = 1) (huv : inner ℝ u v = 0)
    {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
    {f : E → ℝ} (hf : ContDiffOn ℝ ∞ f U) :
    (∫ e : sphere (0 : E) 1, fderiv ℝ f e (rotationGenerator u v e)
      ∂volume.toSphere) = 0 := by
…

Mentions: OAI.AffineBernstein.rotationGenerator