DyadicRadialFits.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual radial targets at successive dyadic source scales

theorem OAI.RegularPointCoordinates.distanceSourceRadius_testing_shift line 15
Source documentation
The fixed testing fraction commutes with every dyadic scale shift.
```
theorem distanceSourceRadius_testing_shift (r0 : ℝ) (i m : ℕ) :
    distanceSourceRadius r0 (i + m) / 64 =
      (1 / 2 : ℝ) ^ m * (distanceSourceRadius r0 i / 64) := by
…
```
Mentions: OAI.RegularPointCoordinates.distanceSourceRadius
theorem OAI.RegularPointCoordinates.distanceSourceRadius_antitone line 22
def OAI.RegularPointCoordinates.DyadicDistanceReplacements.distanceDatum line 35
Source documentation
The canonical compact squared-distance datum at this source scale.
```
def distanceDatum {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.distanceDatum_pairing_later line 44
Source documentation
On a later testing ball every earlier datum gives the same radial pairing. This identifies the actual targets in the lagged recurrence.
```
theorem distanceDatum_pairing_later {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) {i j : ℕ} (hij : i ≤ j)
    (a : SobolevSpace μ hQ) :
    localGamma μ hQ (T.distanceDatum μ hQ i) a =ᵐ[μ.restrict (ball p (distanceSourceRadius r0 j / 64))]
      localGamma μ hQ (T.distanceDatum μ hQ j) a := by
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.distanceSourceRadius

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.distanceDatum_fit_later line 58

Source documentation

Changing to the next canonical source datum preserves the actual least-squares fit on its testing ball.

theorem distanceDatum_fit_later {n k : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) {i j : ℕ} (hij : i ≤ j)
    (u : Fin k → SobolevSpace μ hQ) (a : SobolevSpace μ hQ)
    (hfin : μ (ball p (distanceSourceRadius r0 j / 64)) ≠ ∞) {A A' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict (ball p (distanceSourceRadius r0 j / 64)), localGamma μ hQ a a x ≤ A)
    (ha' : ∀ᵐ x ∂μ.restrict (ball p (distanceSourceRadius r0 j / 64)), localGamma μ hQ a a x ≤ A') :
    radialFitError μ hQ u p (distanceSourceRadius r0 j / 64) hfin (T.distanceDatum μ hQ i) a ha =
      radialFitError μ hQ u p (distanceSourceRadius r0 j / 64) hfin (T.distanceDatum μ hQ j) a ha' :=
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.radialFitError