OAI/Analysis/AncientFlat/Energy/EnergyGradient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParametrixUniqueness.basisVec line 10
2. def OAI.ParametrixUniqueness.gradMass line 11
3. lemma OAI.ParametrixUniqueness.basisVec_norm line 13
4. lemma OAI.ParametrixUniqueness.gradMass_nonneg line 15
5. lemma OAI.ParametrixUniqueness.gradient_balance_dir line 17
6. lemma OAI.ParametrixUniqueness.pair_laplacian line 38
7. lemma OAI.ParametrixUniqueness.gradient_balance line 49
8. lemma OAI.ParametrixUniqueness.gradient_cross_bound line 55
9. lemma OAI.ParametrixUniqueness.cross_comm line 75
10. lemma OAI.ParametrixUniqueness.gradient_interpolation line 78