OAI/Analysis/AffineBernstein/PositiveMassAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The first missing differential identity in sections/area.tex, Stationarity: the cofactor of an actual Hessian is divergence-free. The proof below uses multilinearity of the determinant and symmetry of second derivatives (Piola).

  1. lemma OAI.AffineBernstein.ofReal_integral_le_lintegral_of_nonneg line 15
  2. lemma OAI.AffineBernstein.exists_pos_lower_of_rpow line 22
  3. lemma OAI.AffineBernstein.logTubeMeasure_cell_le_apply line 37