OAI/Geometry/RCD/Coordinates/DyadicFitVolumeUnits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.radial_sqrt_volume_ratio line 9
2. theorem OAI.RegularPointCoordinates.radial_covector_fit_natural_units line 20

   Source documentation

   The actual covector error has one coefficient independent of the center and dyadic scale; its only variable source is sqrt(P) times the norm of the covector in the current normalizing frame.

   theorem radial_covector_fit_natural_units {s theta V Lambda A D N W Q b E F : ℝ}
       (hs : 0 < s) (htheta : 0 < theta) (hV : 0 ≤ V) (hQ : 0 ≤ Q)
       (hA : 0 ≤ A) (hD : 0 ≤ D) (hb : 0 ≤ b) (hVL : V ≤ Lambda) (hratio : N / W ≤ D)
       (hstep : F ≤ (V + (1 / 2 : ℝ) * theta * Real.sqrt theta) / (theta * (s / 64)) *
         Real.sqrt (W⁻¹ * (A * s ^ 2 * (N * Q)) * b ^ 2) +
         (1 / 2 : ℝ) * Real.sqrt theta * E) :
       F ≤ (1 / 2 : ℝ) * Real.sqrt theta * E +
         (64 / theta) * (Lambda + (1 / 2 : ℝ) * theta * Real.sqrt theta) *
           Real.sqrt (A * D) * Real.sqrt Q * b := by
   …