AngularCalculus.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.tangentProjection line 16
Source comment
Orthogonal tangential projection when `e` is a unit vector.
```
def tangentProjection (e v : E) : E := v - inner ℝ e v • e
```
def OAI.AffineBernstein.sphereGradient line 19
Source comment
The ambient extension of the spherical gradient of a degree-one support function.
```
def sphereGradient (H : E → ℝ) (e : E) : E := gradient H e - H e • e
```
def OAI.AffineBernstein.roundDerivative line 22
Source comment
The round covariant derivative, using tangential projection of the ambient derivative.
```
def roundDerivative (V : E → E) (e v : E) : E :=
…
```
def OAI.AffineBernstein.sphereHessian line 26
Source comment
The spherical Hessian evaluated on tangent vectors.
```
def sphereHessian (H : E → ℝ) (e v w : E) : ℝ :=
…
```
def OAI.AffineBernstein.sphereRadius line 29
theorem OAI.AffineBernstein.inner_tangentProjection line 33
theorem OAI.AffineBernstein.tangentProjection_eq line 38
theorem OAI.AffineBernstein.gauss_reconstruction line 41
theorem OAI.AffineBernstein.sphereRadius_eq_hessian line 47
Source comment
`∇²_S h + h Id` is the restriction of the ambient Hessian of the one-homogeneous support function.
```
theorem sphereRadius_eq_hessian {H : E → ℝ} {e : E}
    (hh : ContDiffAt ℝ ∞ H e) (v w : E) (hw : inner ℝ e w = 0) :
    sphereRadius H e v w = fderiv ℝ (fderiv ℝ H) e v w := by
…
```
Mentions: OAI.AffineBernstein.sphereRadius
theorem OAI.AffineBernstein.hasFDerivAt_tangentProjection line 65
Source comment
The standard projected local extension of a tangent vector. At a unit `e`, its round covariant derivative vanishes if `v` is tangent at `e`.
```
theorem hasFDerivAt_tangentProjection (e v : E) :
    HasFDerivAt (fun x => tangentProjection x v)
      (-(inner ℝ e v • ContinuousLinearMap.id ℝ E +
        (InnerProductSpace.toDual ℝ E v).smulRight e)) e := by
…
```
Mentions: OAI.AffineBernstein.tangentProjection
def OAI.AffineBernstein.roundTensorDerivative line 78
Source comment
The covariant derivative of an ambient two-tensor restricted to the sphere. The arguments `u,v,w` are tangent at the unit point of evaluation. The projected constant extensions of `v,w` have zero covariant derivative there.
```
def roundTensorDerivative (A : E → E →L[ℝ] E →L[ℝ] ℝ) (e u v w : E) : ℝ :=
…
```
theorem OAI.AffineBernstein.roundTensorDerivative_eq line 81

theorem OAI.AffineBernstein.supportRadius_codazzi line 101

Source comment

Codazzi for the radius tensor of a smooth one-homogeneous support function. The radial Hessian identity is precisely the derivative of Euler's identity; there is no assumed Codazzi equation.

theorem supportRadius_codazzi {H : E → ℝ} {e : E}
    (hh : ContDiffAt ℝ ∞ H e)
    (hrad : ∀ v, fderiv ℝ (fderiv ℝ H) e v e = 0)
    (u v w : E) (hu : inner ℝ e u = 0) (hv : inner ℝ e v = 0)
    (hw : inner ℝ e w = 0) :
    roundTensorDerivative (fderiv ℝ (fderiv ℝ H)) e u v w =
      roundTensorDerivative (fderiv ℝ (fderiv ℝ H)) e v u w := by
…

Mentions: OAI.AffineBernstein.roundTensorDerivative