OAI/Analysis/CoulombIonization/Localization/SqrtMultiplier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombObservation.sqrt_lipschitz_of_fderiv_bound line 17
2. lemma OAI.CoulombObservation.lineDeriv_sqrt_of_pos line 45
3. lemma OAI.CoulombObservation.lineDeriv_sqrt_of_zero line 53
4. def OAI.CoulombObservation.sqrtLikelihoodLipschitzConstant line 69
5. lemma OAI.CoulombObservation.arrayLikelihood_fderiv_norm line 74
6. lemma OAI.CoulombObservation.sqrtArrayLikelihood_lipschitz line 112
7. lemma OAI.CoulombObservation.sqrtArrayLikelihood_lineDeriv_sq line 127