GramDirectionalError.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

From coordinatewise Gram errors to every constant direction

theorem OAI.RegularPointCoordinates.gamma_sum_left line 17
theorem OAI.RegularPointCoordinates.gamma_sum_right line 31
Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/RadialLinearCombination.lean:17 (same statement text; different proof or body). Qualify references as OAI.RegularPointCoordinates.gamma_sum_right@path.
theorem OAI.RegularPointCoordinates.localGamma_column_pair line 46
Source documentation
Finite coordinate expansion of the actual local carré du champ.
```
theorem localGamma_column_pair {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (v w : Euclidean n) :
    localGamma μ hQ (sobolevColumnMap μ hQ u v) (sobolevColumnMap μ hQ u w) =ᵐ[μ]
      fun x => ∑ i : Fin n, ∑ j : Fin n, (v i * w j) * localGamma μ hQ (u i) (u j) x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap
theorem OAI.RegularPointCoordinates.integral_abs_sum_le line 88

theorem OAI.RegularPointCoordinates.directional_gram_error_le line 100

Source documentation

Coordinatewise L1 Gram errors control the error in every constant direction, with one dimension-dependent factor and the squared norm of the direction. This supplies the directional premise of the mass estimate.

theorem directional_gram_error_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (S : Set X) (hSfin : μ S ≠ ∞) {epsilon : ℝ} (heps : 0 ≤ epsilon)
    (herror : ∀ i j : Fin n, ∫ x in S,
      |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ epsilon)
    (v : Euclidean n) :
    (∫ x in S, |localGamma μ hQ (sobolevColumnMap μ hQ u v)
      (sobolevColumnMap μ hQ u v) x - ‖v‖ ^ 2| ∂μ) ≤
      (n : ℝ) ^ 2 * epsilon * ‖v‖ ^ 2 := by
…

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