OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.RadialPotential.hermitianLog_ddc_perturbation line 17
2. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrt_ddc_perturbation line 51
3. lemma OAI.TamingCompatibility.RadialPotential.hermitianLog_variable_ddc_lower line 95
4. lemma OAI.TamingCompatibility.RadialPotential.hermitian_sqrt_radius_bound line 109
5. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrt_variable_ddc_lower line 123
6. lemma OAI.TamingCompatibility.RadialPotential.hermitian_log_trace_inner line 143