FramedRadialValue.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The Poisson radial value estimate in its normalizing frame

theorem OAI.RegularPointCoordinates.framed_directional_gradient line 18

Source documentation

The original coordinate covector has the gradient bound supplied by its inverse normalizing frame.

theorem framed_directional_gradient {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (s : Set X) (L : ℝ)
    (hgrad : ∀ j, ∀ᵐ x ∂μ.restrict s,
      localGamma μ hQ (transformedColumn μ hQ u N j)
        (transformedColumn μ hQ u N j) x ≤ L ^ 2) (b : Euclidean n) :
    ∀ᵐ x ∂μ.restrict s,
      localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤
        ((n : ℝ) * L) ^ 2 * ‖N.symm b‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.framed_value_transfer line 34
Source documentation
Transfer any actual distance fit to the same Poisson pairing. The only new term is the already constructed Poisson energy error.
```
theorem DyadicDistanceReplacements.framed_value_transfer
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    {L : ℝ}
    (hgrad : ∀ j, ∀ᵐ x ∂μ.restrict (ball p (distanceSourceRadius r0 i / 64)),
      localGamma μ hQ (transformedColumn μ hQ u N j)
        (transformedColumn μ hQ u N j) x ≤ L ^ 2)
    (b : Euclidean n)
    (G : LocalHessianPairing μ hQ (ball p (distanceSourceRadius r0 i / 64))
      (T.replacement i) (sobolevColumnMap μ hQ u b))
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.sobolevColumnMap