OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianFarSmooth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.ExteriorForms.parameter_fderiv_contDiffAt line 19
2. lemma OAI.TamingCompatibility.ExteriorForms.parameter_dc_contDiffAt line 26
3. lemma OAI.TamingCompatibility.ExteriorForms.parameter_ddc_contDiffAt line 34
4. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog_joint_smooth line 51
5. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt_joint_smooth line 66
6. lemma OAI.TamingCompatibility.HermitianRadial.far_parameter_compact line 97
7. lemma OAI.TamingCompatibility.HermitianRadial.cutoffLog_ddc_far_bound line 108
8. lemma OAI.TamingCompatibility.HermitianRadial.cutoffSqrt_ddc_far_bound line 134
9. lemma OAI.TamingCompatibility.HermitianRadial.log_distance_far_bound line 160