CenteredProjectionRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting the actual radial rows to the centered projection coordinates

theorem OAI.RegularPointCoordinates.centered_affine_restrict_cutoff_eq line 20

Source documentation

Changing the representative of the local constant preserves the restricted centered affine function.

theorem centered_affine_restrict_cutoff_eq {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (z a : Euclidean n)
    (s : Set X) (hs : μ s ≠ ∞) (eta chi : SobolevSpace μ hQ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict s] fun _ => (1 : ℝ))
    (hchi : SobolevSpace.toLp μ hQ chi =ᵐ[μ.restrict s] fun _ => (1 : ℝ)) :
    SobolevSpace.restrictLp μ hQ s (centeredAffineSobolev μ hQ u eta z a) =
      SobolevSpace.restrictLp μ hQ s (centeredAffineSobolev μ hQ u chi z a) := by
…

theorem OAI.RegularPointCoordinates.normalized_centered_frame_fit line 35

Source documentation

A row fit on the radial ball transfers to the smaller projection ball and to the centered exact frame, with just the volume-ratio loss.

theorem normalized_centered_frame_fit {n : ℕ} {s t : Set X} (hts : t ⊆ s)
    (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) (hs0 : 0 < μ.real s) (ht0 : 0 < μ.real t)
    (u : Fin n → SobolevSpace μ hQ) (g eta chi : SobolevSpace μ hQ)
    (N : Euclidean n ≃L[ℝ] Euclidean n) (z a : Euclidean n)
    {C E : ℝ} (hE : 0 ≤ E) (hvol : μ.real s ≤ C * μ.real t)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict t] fun _ => (1 : ℝ))
    (hchi : SobolevSpace.toLp μ hQ chi =ᵐ[μ.restrict t] fun _ => (1 : ℝ))
    (hfit : ‖normalizeLocalL2 μ s hs (SobolevSpace.restrictLp μ hQ s
      (g - centeredAffineSobolev μ hQ u chi z a))‖ ^ 2 ≤ E) :
    let uc := centeredColumn μ hQ (transformedColumn μ hQ u N)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.centeredAffineSobolev, OAI.RegularPointCoordinates.centeredColumn, OAI.RegularPointCoordinates.transformedColumn

theorem OAI.RegularPointCoordinates.centered_radial_representative line 61

Source documentation

Centering a coordinate changes its local representative by a constant and therefore preserves its pairing with the actual Poisson gradient.

theorem centered_radial_representative {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (f g eta : SobolevSpace μ hQ)
    (z : Euclidean n) (s : Set X) (j : Fin n)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict s] fun _ => (1 : ℝ))
    (hrep : SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict s]
      localGamma μ hQ f (u j)) :
    SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict s]
      localGamma μ hQ f (centeredColumn μ hQ u z eta j) := by
…