ProjectionRadialRows.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual row fits in the centered normalized projection coordinates

theorem OAI.RegularPointCoordinates.centered_normalized_radial_values line 20

Source documentation

Only the scalar value fits are needed to build the radial operator used in sharp projection.

theorem centered_normalized_radial_values {n : ℕ}
    (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (u g : Fin n → SobolevSpace μ hQ) (f eta : SobolevSpace μ hQ)
    (N : Euclidean n ≃L[ℝ] Euclidean n) (z : Euclidean n)
    (coeff : Fin n → Euclidean n) {E B : ℝ} (hE : 0 ≤ E)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (g j) =ᵐ[μ.restrict Ω]
      localGamma μ hQ f (transformedColumn μ hQ u N j))
    (hvalue : ∀ j, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (g j - centeredAffineSobolev μ hQ u eta z (coeff j)))‖ ^ 2 ≤ E) :
    let uc := centeredColumn μ hQ (transformedColumn μ hQ u N)
…

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

theorem OAI.RegularPointCoordinates.centered_normalized_radial_rows line 67

Source documentation

The dyadic row fits provide one genuine radial derivative operator and one coefficient operator in the centered normalized coordinates. The same residual controls values and energy for every covector.

theorem centered_normalized_radial_rows {n : ℕ}
    (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (u g : Fin n → SobolevSpace μ hQ) (f eta : SobolevSpace μ hQ)
    (N : Euclidean n ≃L[ℝ] Euclidean n) (z : Euclidean n)
    (coeff : Fin n → Euclidean n) {E D B : ℝ} (hE : 0 ≤ E) (_hD : 0 ≤ D)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (g j) =ᵐ[μ.restrict Ω]
      localGamma μ hQ f (transformedColumn μ hQ u N j))
    (hvalue : ∀ j, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (g j - centeredAffineSobolev μ hQ u eta z (coeff j)))‖ ^ 2 ≤ E)
    (henergy : ∀ j, (μ.real Ω)⁻¹ * ∫ x in Ω,
…