TensorIntegration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.integral_roundHessianContraction line 21

Source comment

Weighted spherical tensor integration by parts, for the literal round measure. All smoothness and integrability statements are derived on a neighborhood of the compact sphere.

theorem integral_roundHessianContraction (b : OrthonormalBasis ι ℝ E)
    {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
    {T : E → E →L[ℝ] E →L[ℝ] ℝ} (hT : ContDiffOn ℝ ∞ T U)
    (hr : ∀ e ∈ sphere (0 : E) 1, ∀ v, inner ℝ e v = 0 → T e e v = 0 ∧ T e v e = 0)
    (hdiv : ∀ e ∈ sphere (0 : E) 1, ∀ v, inner ℝ e v = 0 → (∑ i,
      roundTensorDerivative T e (tangentProjection e (b i)) (tangentProjection e (b i)) v) = 0)
    {f g : E → ℝ} (hf : ContDiffOn ℝ ∞ f U) (hg : ContDiffOn ℝ ∞ g U) :
    (∫ e : sphere (0 : E) 1, f e * roundHessianContraction b T g e ∂volume.toSphere) =
      -(∫ e : sphere (0 : E) 1, T e (tangentProjection e (gradient f e))
        (tangentProjection e (gradient g e)) ∂volume.toSphere) := by
…

Mentions: OAI.AffineBernstein.roundTensorDerivative, OAI.AffineBernstein.tangentProjection, OAI.AffineBernstein.roundHessianContraction

theorem OAI.AffineBernstein.integral_roundHessianContraction_comm line 62

Source comment

The exact twofold angular IBP needed by the tube Euler equation.

theorem integral_roundHessianContraction_comm (b : OrthonormalBasis ι ℝ E)
    {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
    {T : E → E →L[ℝ] E →L[ℝ] ℝ} (hT : ContDiffOn ℝ ∞ T U)
    (hs : ∀ e ∈ sphere (0 : E) 1, ∀ v w, T e v w = T e w v)
    (hr : ∀ e ∈ sphere (0 : E) 1, ∀ v, inner ℝ e v = 0 → T e e v = 0 ∧ T e v e = 0)
    (hdiv : ∀ e ∈ sphere (0 : E) 1, ∀ v, inner ℝ e v = 0 → (∑ i,
      roundTensorDerivative T e (tangentProjection e (b i)) (tangentProjection e (b i)) v) = 0)
    {f g : E → ℝ} (hf : ContDiffOn ℝ ∞ f U) (hg : ContDiffOn ℝ ∞ g U) :
    (∫ e : sphere (0 : E) 1, f e * roundHessianContraction b T g e ∂volume.toSphere) =
      ∫ e : sphere (0 : E) 1, g e * roundHessianContraction b T f e ∂volume.toSphere := by
…

Mentions: OAI.AffineBernstein.roundTensorDerivative, OAI.AffineBernstein.tangentProjection, OAI.AffineBernstein.roundHessianContraction

theorem OAI.AffineBernstein.integral_supportNewtonTensor_by_parts line 80

Source comment

For the actual Newton/cofactor of a radial homogeneous Hessian, both tensor hypotheses of angular integration by parts are PRODUCED, not postulated.

theorem integral_supportNewtonTensor_by_parts (b : OrthonormalBasis ι ℝ E)
    {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
    {H : E → ℝ} (hH : ContDiffOn ℝ ∞ H U)
    (hr : ∀ q ∈ U, ∀ v, fderiv ℝ (fderiv ℝ H) q v q = 0)
    {f g : E → ℝ} (hf : ContDiffOn ℝ ∞ f U) (hg : ContDiffOn ℝ ∞ g U) :
    (∫ e : sphere (0 : E) 1, f e *
      roundHessianContraction b (supportNewtonTensor b H) g e ∂volume.toSphere) =
      -(∫ e : sphere (0 : E) 1, supportNewtonTensor b H e
        (tangentProjection e (gradient f e)) (tangentProjection e (gradient g e)) ∂volume.toSphere) := by
…

Mentions: OAI.AffineBernstein.roundHessianContraction, OAI.AffineBernstein.supportNewtonTensor, OAI.AffineBernstein.tangentProjection