OAI/Geometry/NodalSets/Coefficients/CorrectionAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Yau.correction_denominator_pos line 10
2. theorem OAI.Yau.exact_correction line 18
3. theorem OAI.Yau.simplicity_preserves line 29
4. theorem OAI.Yau.simplicity_energy_integrand line 35
5. theorem OAI.Yau.first_jet_coercivity line 40
6. theorem OAI.Yau.reciprocal_exponent line 48
7. theorem OAI.Yau.correction_accuracy line 51