OAI/Geometry/TamingCompatibility/DifferentialForms/TwoDirection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.RadialPotential.two_direction_inner_sq_le line 12
2. lemma OAI.TamingCompatibility.RadialPotential.logPotential_trace_lower line 36
3. lemma OAI.TamingCompatibility.RadialPotential.sqrtPotential_trace_lower line 51
4. lemma OAI.TamingCompatibility.RadialPotential.logPotential_smooth line 81
5. lemma OAI.TamingCompatibility.RadialPotential.sqrtPotential_smooth line 86
6. lemma OAI.TamingCompatibility.RadialPotential.constant_ddc_trace line 89
7. lemma OAI.TamingCompatibility.RadialPotential.orthogonal_complex_pair line 97
8. lemma OAI.TamingCompatibility.RadialPotential.log_ddc_lower line 108
9. lemma OAI.TamingCompatibility.RadialPotential.sqrt_ddc_lower line 120
10. lemma OAI.TamingCompatibility.RadialPotential.bilinear_diagonal_difference line 141
11. lemma OAI.TamingCompatibility.RadialPotential.ddc_gradient_bound line 162
12. lemma OAI.TamingCompatibility.RadialPotential.ddc_perturbation_bound line 175