RadialLinearCombination.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Radial pairings and harmonic corrections in every constant direction

theorem OAI.RegularPointCoordinates.gamma_sum_right line 17
Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/GramDirectionalError.lean:31 (same statement text; different proof or body). Qualify references as OAI.RegularPointCoordinates.gamma_sum_right@path.
theorem OAI.RegularPointCoordinates.localGamma_column_right line 32
Source documentation
The radial derivative is linear in the actual coordinate direction.
Distinct definitions of this name: OAI/Geometry/RCD/Sobolev/GammaColumnMixed.lean:13 (different declaration text). Qualify references as OAI.RegularPointCoordinates.localGamma_column_right@path.
```
theorem localGamma_column_right {n : ℕ} (q : SobolevSpace μ hQ)
    (u : Fin n → SobolevSpace μ hQ) (b : Euclidean n) :
    localGamma μ hQ q (sobolevColumnMap μ hQ u b) =ᵐ[μ]
      fun x => ∑ j, b j * localGamma μ hQ q (u j) x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap
theorem OAI.RegularPointCoordinates.column_value line 45

theorem OAI.RegularPointCoordinates.radial_linear_harmonic_correction line 56

Source documentation

Componentwise harmonic corrections give one correction in every constant direction, with the finite-dimensional Cauchy--Schwarz loss.

theorem radial_linear_harmonic_correction {n : ℕ} {Ω : Set X}
    (q : SobolevSpace μ hQ) (u h : Fin n → SobolevSpace μ hQ)
    (hh : ∀ j, IsSobolevHarmonicOn μ hQ Ω (h j))
    (hm : ∀ j, MemLp (fun x => localGamma μ hQ q (u j) x -
      SobolevSpace.toLp μ hQ (h j) x) 2 (μ.restrict Ω))
    {E : ℝ}
    (he : ∀ j, (∫ x in Ω, (localGamma μ hQ q (u j) x -
      SobolevSpace.toLp μ hQ (h j) x) ^ 2 ∂μ) ≤ E)
    (b : Euclidean n) :
    IsSobolevHarmonicOn μ hQ Ω (sobolevColumnMap μ hQ h b) ∧
    (∫ x in Ω, (localGamma μ hQ q (sobolevColumnMap μ hQ u b) x -
      SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ h b) x) ^ 2 ∂μ) ≤
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap