SphereAlgebra.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.roundDivergence line 16
Source comment
Ambient expression for the round divergence of the restriction to the unit sphere.
```
def roundDivergence (b : OrthonormalBasis ι ℝ E) (W : E → E) (e : E) : ℝ :=
…
```
theorem OAI.AffineBernstein.rotationGenerator_apply line 19
theorem OAI.AffineBernstein.sum_rotation_pair_first line 22
theorem OAI.AffineBernstein.sum_rotation_pair_second line 37
theorem OAI.AffineBernstein.roundDivergence_trace line 60

theorem OAI.AffineBernstein.sum_rotation_pair line 68

Source comment

Contraction of the rotation derivatives is divergence minus the normal correction.

theorem sum_rotation_pair (b : OrthonormalBasis ι ℝ E) (e : E)
    (he : inner ℝ e e = 1) (w : E) (M : E →L[ℝ] E) :
    (∑ i, ∑ j, (inner ℝ (b i) (rotationGenerator (b i) (b j) e) * inner ℝ (b j) w +
      inner ℝ (b i) e * inner ℝ (b j) (M (rotationGenerator (b i) (b j) e)))) =
      (∑ j, inner ℝ (b j) (M (b j))) - inner ℝ e (M e) +
        (1 - (Fintype.card ι : ℝ)) * inner ℝ e w := by
…

Mentions: OAI.AffineBernstein.rotationGenerator