ActualProjectionThreshold.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A geometric smallness threshold for the actual sharp projection

theorem OAI.RegularPointCoordinates.actual_projection_error_threshold line 20
Source documentation
Small metric-approximation error and small total original source mass make the constructed joint compactness error uniformly small.
```
theorem actual_projection_error_threshold (hB : 0 ≤ B) {delta : ℝ} (hdelta : 0 < delta) :
    ∃ tau : ℝ, 0 < tau ∧ ∀ d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M,
      d.approximationError ≤ tau → d.totalSource ≤ tau → d.error < delta := by
…
```
Mentions: OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.ActualProjectionConfiguration

theorem OAI.RegularPointCoordinates.actual_sharp_projection_small_data line 57

Source documentation

The sharp bound now requires only separate geometric approximation and original source tolerances, as supplied by the regular-neighborhood construction.

theorem actual_sharp_projection_small_data
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX) (hn : 2 ≤ n)
    (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hJ : 0 ≤ J)
    (hCχ : 0 ≤ Cχ) (hA : 0 ≤ A) (hepsilon : 0 ≤ epsilon)
    (hH : 0 ≤ H) (hD : 0 ≤ D) (hL : 0 ≤ L) :
    ∃ P tau : ℝ, 0 < P ∧ 0 < tau ∧
      ∀ d : ActualProjectionConfiguration hX κ B J C A Cχ epsilon H D L M,
        d.approximationError ≤ tau → d.totalSource ≤ tau → d.projectionNorm ≤ P * d.source := by
…

Mentions: OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput, OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.ActualProjectionConfiguration