RadialVolumeUnits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed volume losses for the actual radial fit

theorem OAI.RegularPointCoordinates.quarter_volume_bounds line 9

theorem OAI.RegularPointCoordinates.radial_testing_volume_ratio line 22

Source documentation

At the fixed radial testing fraction, the source normalization and the averaging normalization differ by a dimensional constant.

theorem radial_testing_volume_ratio {n : ℕ} {s omega V : ℝ}
    (hs : 0 < s) (homega : 0 < omega)
    (h : |V / (omega * (s / 64) ^ n) - 1| ≤ 1 / 4) :
    s ^ (n : ℝ) / V ≤ (4 / (3 * omega)) * (64 : ℝ) ^ n := by
…

theorem OAI.RegularPointCoordinates.radial_fraction_volume_ratio line 36

Source documentation

Both radius levels lie in the same quarter-error volume regime.

theorem radial_fraction_volume_ratio {n : ℕ} {r theta omega V W : ℝ}
    (hr : 0 < r) (htheta : 0 < theta) (homega : 0 < omega)
    (hV : |V / (omega * r ^ n) - 1| ≤ 1 / 4)
    (hW : |W / (omega * (theta * r) ^ n) - 1| ≤ 1 / 4) :
    V / W ≤ (5 / 3 : ℝ) * (theta ^ n)⁻¹ := by
…

theorem OAI.RegularPointCoordinates.radial_sqrt_error_bound line 52

Source documentation

The normalized integral error has size at most s*sqrt(P), with one fixed coefficient. This is the error inserted into the dyadic fit step.

theorem radial_sqrt_error_bound {s V Q C D : ℝ}
    (hs : 0 ≤ s) (hQ : 0 ≤ Q) (hC : 0 ≤ C) (hD : 0 ≤ D)
    {N : ℝ} (hratio : N / V ≤ D) :
    Real.sqrt (V⁻¹ * (C * s ^ 2 * (N * Q))) ≤ s * Real.sqrt (C * D) * Real.sqrt Q := by
…

theorem OAI.RegularPointCoordinates.radial_fit_rescale line 65

Source documentation

Dividing the fitted values by their own radii gives the strict square-root contraction factor. The 64 is the fixed testing fraction.

theorem radial_fit_rescale {s theta Lambda A Q E F : ℝ}
    (hs : 0 < s) (htheta : 0 < theta)
    (hstep : F ≤ (Lambda + (1 / 2 : ℝ) * theta * Real.sqrt theta) *
      s * A * Real.sqrt Q + (1 / 2 : ℝ) * theta * Real.sqrt theta * E) :
    F / (theta * (s / 64)) ≤ (1 / 2 : ℝ) * Real.sqrt theta * (E / (s / 64)) +
      (64 / theta) * (Lambda + (1 / 2 : ℝ) * theta * Real.sqrt theta) * A * Real.sqrt Q := by
…

theorem OAI.RegularPointCoordinates.radial_fit_natural_units line 77

Source documentation

The actual normalized volume bound removes all scale dependence from the affine-fit error. This is the scalar recurrence used by the envelope.

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