OAI/Geometry/TamingCompatibility/DifferentialForms/RadialObserverScale.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.RadialPotential.observerScale line 10
2. lemma OAI.TamingCompatibility.RadialPotential.observerScale_properties line 12
3. lemma OAI.TamingCompatibility.RadialPotential.observerScale_le_dist line 36
4. lemma OAI.TamingCompatibility.RadialPotential.inverse_observer_to_distance line 41
5. lemma OAI.TamingCompatibility.RadialPotential.log_abs_comparison line 49
6. lemma OAI.TamingCompatibility.RadialPotential.log_observer_to_distance line 63
7. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_logSource_distance_estimate line 116
8. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_sqrtSource_distance_estimate line 149