ActualProjectionConfiguration.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The geometric data for one actual two-center projection

The source measures, equal-Laplacian Poisson replacements and harmonic coordinate estimates determine the affine projection and its residual.

structure OAI.RegularPointCoordinates.ActualProjectionConfiguration line 24
Source documentation
Equal-Laplacian replacements and harmonic coordinates centered at the second point, with their source and normalization bounds.
```
structure ActualProjectionConfiguration {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    [IsFiniteMeasureOnCompacts (hausdorff n X)] (κ B J C A Cχ epsilon H D L M : ℝ) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff
def OAI.RegularPointCoordinates.ActualProjectionConfiguration.radius line 113
Source documentation
The physical radius is the actual radius of the chosen replacement.
```
def radius (d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.ActualProjectionConfiguration
theorem OAI.RegularPointCoordinates.ActualProjectionConfiguration.radius_pos line 116
theorem OAI.RegularPointCoordinates.ActualProjectionConfiguration.radius_le_root line 119
def OAI.RegularPointCoordinates.ActualProjectionConfiguration.error line 127
Source documentation
One explicit approximation error controls both the measured coordinates and the actual radial quadratic error.
```
def error (d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.ActualProjectionConfiguration
theorem OAI.RegularPointCoordinates.ActualProjectionConfiguration.approximationError_le line 133
theorem OAI.RegularPointCoordinates.ActualProjectionConfiguration.error_pos line 145

theorem OAI.RegularPointCoordinates.ActualProjectionConfiguration.quadratic_error line 150

Source documentation

The actual radial quadratic estimate on the outer projection ball.

theorem quadratic_error
    (hn : 2 ≤ n) (hκ : 0 ≤ κ) (hB : 0 ≤ B)
    (d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M) :
    ((hausdorff n X).real (ball d.center ((1 / 1024) * d.radius)))⁻¹ *
      (∫ x in ball d.center ((1 / 1024) * d.radius),
        (SobolevSpace.toLp (hausdorff n X) hX.quadratic
          ((d.radius ^ 2)⁻¹ • d.secondReplacement.replacement d.index) x -
            ‖d.coordinateValues x‖ ^ 2 / 2) ^ 2 ∂hausdorff n X) ≤ d.error := by
…

Mentions: OAI.RegularPointCoordinates.ActualProjectionConfiguration, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace.toLp

def OAI.RegularPointCoordinates.ActualProjectionConfiguration.projectionNorm line 190
Source documentation
The exact orthogonal residual norm of the actual two-center target.
```
def projectionNorm (d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.ActualProjectionConfiguration