OAI/Analysis/AffineBernstein/ActualTubeMetricPositivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineEpigraph_tube_angular_pair_nonneg line 22
2. lemma OAI.AffineBernstein.gradient_exp_linear_combination line 55
3. lemma OAI.AffineBernstein.tangentProjection_smul_add line 69
4. theorem OAI.AffineBernstein.integral_supportNewtonTensor_exp_weight line 78

   Source comment

   Exact angular weighted integration by parts for the source exponential weight. The cofactor divergence and radial cancellations are proved by the Newton calculus, not included as additional hypotheses.

   theorem integral_supportNewtonTensor_exp_weight (b : OrthonormalBasis ι ℝ E)
       {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
       {H P F : E → ℝ} (hH : ContDiffOn ℝ ∞ H U)
       (hr : ∀ q ∈ U, ∀ v, fderiv ℝ (fderiv ℝ H) q v q = 0)
       (hP : ContDiffOn ℝ ∞ P U) (hF : ContDiffOn ℝ ∞ F U) (a c : ℝ) :
       (∫ e : sphere (0 : E) 1, Real.exp (a*P e+c*F e) *
         roundHessianContraction b (supportNewtonTensor b H) F e ∂volume.toSphere) =
         -(∫ e : sphere (0 : E) 1, Real.exp (a*P e+c*F e) *
           (a * supportNewtonTensor b H e (tangentProjection e (gradient P e))
               (tangentProjection e (gradient F e)) +
            c * supportNewtonTensor b H e (tangentProjection e (gradient F e))
               (tangentProjection e (gradient F e))) ∂volume.toSphere) := by
   …

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

5. lemma OAI.AffineBernstein.sphere_tangent_gradient_continuous line 105
6. lemma OAI.AffineBernstein.sphere_supportNewtonTensor_continuous line 115
7. theorem OAI.AffineBernstein.integral_supportNewtonTensor_weighted_drift line 125

   Source comment

   The angular drift coefficient after integration is exactly `1-c`. At `c=(n+2)/2` this is `-n/2`, as in tubes.tex.

   theorem integral_supportNewtonTensor_weighted_drift (b : OrthonormalBasis ι ℝ E)
       {U : Set E} (hU : IsOpen U) (hSU : sphere (0 : E) 1 ⊆ U)
       {H P F : E → ℝ} (hH : ContDiffOn ℝ ∞ H U)
       (hr : ∀ q ∈ U, ∀ v, fderiv ℝ (fderiv ℝ H) q v q = 0)
       (hP : ContDiffOn ℝ ∞ P U) (hF : ContDiffOn ℝ ∞ F U) (a c : ℝ) :
       (∫ e : sphere (0 : E) 1, Real.exp (a*P e+c*F e) *
         roundHessianContraction b (supportNewtonTensor b H) F e ∂volume.toSphere) +
       a*(∫ e : sphere (0 : E) 1, Real.exp (a*P e+c*F e) *
         supportNewtonTensor b H e (tangentProjection e (gradient P e))
           (tangentProjection e (gradient F e)) ∂volume.toSphere) +
       (∫ e : sphere (0 : E) 1, Real.exp (a*P e+c*F e) *
         supportNewtonTensor b H e (tangentProjection e (gradient F e))
   …

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