OAI/Geometry/TamingCompatibility/DifferentialForms/AntiDdcBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ExteriorForms.antiDdc_vector_bound line 17
2. lemma OAI.TamingCompatibility.ExteriorForms.norm_anti_ddc_evaluation_le line 37
3. lemma OAI.TamingCompatibility.ManifoldForms.ddc_smooth_closed line 56
4. lemma OAI.TamingCompatibility.ManifoldForms.norm_anti_ddc_chart_le line 63
5. def OAI.TamingCompatibility.RadialPotential.logPotential line 97
6. def OAI.TamingCompatibility.RadialPotential.sqrtPotential line 98
7. lemma OAI.TamingCompatibility.RadialPotential.radial_sq_pos line 101
8. lemma OAI.TamingCompatibility.RadialPotential.logPotential_fderiv line 103
9. lemma OAI.TamingCompatibility.RadialPotential.sqrtPotential_fderiv line 112
10. lemma OAI.TamingCompatibility.RadialPotential.logPotential_hessian line 121
11. lemma OAI.TamingCompatibility.RadialPotential.sqrtPotential_hessian line 137