OAI/Geometry/TamingCompatibility/DifferentialForms/RadialLower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.RadialPotential.log_variable_ddc_lower line 17
2. lemma OAI.TamingCompatibility.RadialPotential.sqrt_variable_ddc_lower line 31
3. lemma OAI.TamingCompatibility.RadialPotential.log_trace_inner_ball line 54
4. def OAI.TamingCompatibility.RadialPotential.annularParameters line 74
5. lemma OAI.TamingCompatibility.RadialPotential.annularParameters_positive line 78
6. lemma OAI.TamingCompatibility.RadialPotential.log_joint_smooth_at line 84
7. lemma OAI.TamingCompatibility.RadialPotential.sqrt_joint_smooth_at line 90
8. lemma OAI.TamingCompatibility.RadialPotential.annularParameters_compact line 97
9. lemma OAI.TamingCompatibility.RadialPotential.log_annular_derivatives_bounded line 100
10. lemma OAI.TamingCompatibility.RadialPotential.sqrt_annular_derivatives_bounded line 113
11. lemma OAI.TamingCompatibility.RadialPotential.logPotential_radial_scale line 125
12. lemma OAI.TamingCompatibility.RadialPotential.sqrtPotential_radial_scale line 133