OAI/Geometry/RCD/Harmonic/DirectionRecoveryScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.directionRecoveryError line 9
2. def OAI.RegularPointCoordinates.directionRecoveryConstant line 12
3. theorem OAI.RegularPointCoordinates.direction_recovery_scaled_error line 17

   Source documentation

   The error obtained from the actual radial fits has one length factor and one square root of the original pair source envelope.

   theorem direction_recovery_scaled_error {s A V E C x z p : ℝ}
       (hs : 0 < s) (hA : 0 ≤ A) (hV : 0 ≤ V) (hE : 0 ≤ E) (hC : 0 ≤ C)
       (hx : 0 ≤ x) (hz : 0 ≤ z) (_hp : 0 ≤ p) (hpS : p ≤ x + z) :
       (2 * A * s) * Real.sqrt (E * z) + Real.sqrt (C * s ^ 2 * p) +
         (A * s) * Real.sqrt (2 * (E * z) + 2 * (E * x)) +
         Real.sqrt (2 * (V * s ^ 2 * z) + 2 * (V * s ^ 2 * x)) / 4 ≤
         s * directionRecoveryError A V E C * Real.sqrt (x + z) := by
   …

   Mentions: OAI.RegularPointCoordinates.directionRecoveryError

4. theorem OAI.RegularPointCoordinates.direction_recovery_scaled_bound line 51

   Source documentation

   The reciprocal length from coefficient recovery cancels the length in the error, leaving a uniform physical direction bound.

   theorem direction_recovery_scaled_bound {s A V E C G M x z p : ℝ}
       (hs : 0 < s) (hA : 0 ≤ A) (hV : 0 ≤ V) (hE : 0 ≤ E) (hC : 0 ≤ C)
       (hG : 0 ≤ G) (hM : 0 ≤ M) (hx : 0 ≤ x) (hz : 0 ≤ z)
       (hp : 0 ≤ p) (hpS : p ≤ x + z) :
       let a := 4 * (G / (s / 2048))
   …