OAI/Analysis/AffineBernstein/CapCovariance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affine_area_scaling_identity line 15
2. def OAI.AffineBernstein.affineImageCapArea line 36

   Source documentation

   Affine area of the actual cap, in the original global graph chart. The determinant exponent is the one proved for the literal parametric density.

   def affineImageCapArea {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ) (b : ℝ) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.triangular_area_scaling line 41
4. theorem OAI.AffineBernstein.triangular_graph_cap_area line 65

   Source documentation

   The true cap integral is identical in the sheared graph coordinates.

   theorem triangular_graph_cap_area {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (M : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) {c : ℝ}
       (hc : M (0,1) = (0,c)) (hcp : 0 < c) (v : Space n × ℝ) (b : ℝ) :
       (∫ y in {y | (triangularBaseEquiv M hc hcp.ne').symm (y-v.1) ∈ Ω ∧
           triangularGraphFunction u M hc hcp.ne' v y < b},
          affineAreaDensity (triangularGraphFunction u M hc hcp.ne' v) y) =
         affineImageCapArea Ω u M v b := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.triangularBaseEquiv, OAI.AffineBernstein.triangularGraphFunction, OAI.AffineBernstein.affineAreaDensity, OAI.AffineBernstein.affineImageCapArea

5. lemma OAI.AffineBernstein.affineImageCapArea_shear line 101
6. theorem OAI.AffineBernstein.hessian_eq_second line 115
7. theorem OAI.AffineBernstein.second_fderiv_eq_sum line 125
8. theorem OAI.AffineBernstein.second_fderiv_nonneg line 144
9. theorem OAI.AffineBernstein.second_fderiv_pos line 151