OAI/Analysis/AffineBernstein/SphereDivergence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.fderiv_rotationPair line 19
2. theorem OAI.AffineBernstein.rotationPair_smooth line 33
3. theorem OAI.AffineBernstein.sphere_directional_integrable line 37
4. theorem OAI.AffineBernstein.integral_sphere_rotation_basis line 48
5. theorem OAI.AffineBernstein.integral_roundDivergence line 63

   Source comment

   No angular boundary term: the round divergence of an actual smooth tangent vector field integrates to zero, including the two-point and empty spheres.

   theorem integral_roundDivergence (b : OrthonormalBasis ι ℝ E)
       {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
       {W : E → E} (hW : ContDiffOn ℝ ∞ W U)
       (ht : ∀ e ∈ sphere (0 : E) 1, inner ℝ e (W e) = 0) :
       (∫ e : sphere (0 : E) 1, roundDivergence b W e ∂volume.toSphere) = 0 := by
   …

   Mentions: OAI.AffineBernstein.roundDivergence

6. theorem OAI.AffineBernstein.roundDivergence_smul line 101
7. theorem OAI.AffineBernstein.sphere_fderiv_continuous line 123
8. theorem OAI.AffineBernstein.sphere_roundDivergence_continuous line 131
9. theorem OAI.AffineBernstein.integral_sphere_by_parts line 144

   Source comment

   One genuine spherical integration by parts; all integrability follows from smoothness near the compact sphere.

   theorem integral_sphere_by_parts (b : OrthonormalBasis ι ℝ E)
       {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
       {f : E → ℝ} {W : E → E} (hf : ContDiffOn ℝ ∞ f U) (hW : ContDiffOn ℝ ∞ W U)
       (ht : ∀ e ∈ sphere (0 : E) 1, inner ℝ e (W e) = 0) :
       (∫ e : sphere (0 : E) 1, f e * roundDivergence b W e ∂volume.toSphere) =
         -(∫ e : sphere (0 : E) 1, fderiv ℝ f e (W e) ∂volume.toSphere) := by
   …

   Mentions: OAI.AffineBernstein.roundDivergence