FiniteColumnEnergy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

From finite row errors to every covector in the same frame

theorem OAI.RegularPointCoordinates.localGamma_column_le_diagonal_sum line 19
Source documentation
The energy of a finite coordinate combination is bounded by the sum of the row energies. No pointwise bound on the row errors is needed.
```
theorem localGamma_column_le_diagonal_sum {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (b : Euclidean n) :
    ∀ᵐ x ∂μ, localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤
      (n : ℝ) * ‖b‖ ^ 2 * ∑ j, localGamma μ hQ (u j) (u j) x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap
theorem OAI.RegularPointCoordinates.column_energy_bound line 61
Source documentation
A common bound for the integrated row errors controls every covector error in the same coordinate frame.
```
theorem column_energy_bound {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (Ω : Set X)
    {E : ℝ} (hE : ∀ j, (∫ x in Ω, localGamma μ hQ (u j) (u j) x ∂μ) ≤ E)
    (b : Euclidean n) :
    (∫ x in Ω, localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ∂μ) ≤
      (n : ℝ) ^ 2 * E * ‖b‖ ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.weighted_column_energy_bound line 81

Source documentation

The same estimate works for averaged energy, without requiring the averaging measure to have a strictly positive volume.

theorem weighted_column_energy_bound {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (Ω : Set X) {w E : ℝ} (hw : 0 ≤ w)
    (hE : ∀ j, w * (∫ x in Ω, localGamma μ hQ (u j) (u j) x ∂μ) ≤ E)
    (b : Euclidean n) :
    w * (∫ x in Ω, localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ∂μ) ≤
      (n : ℝ) ^ 2 * E * ‖b‖ ^ 2 := by
…

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

theorem OAI.RegularPointCoordinates.normalized_column_norm_le line 104
Source documentation
Finite rowwise value bounds also control the normalized local L2 value of every coordinate combination.
```
theorem normalized_column_norm_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (Ω : Set X) (hfin : μ Ω ≠ ∞) {D : ℝ}
    (hrow : ∀ j, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (u j))‖ ≤ D)
    (b : Euclidean n) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (sobolevColumnMap μ hQ u b))‖ ≤
      (n : ℝ) * D * ‖b‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.normalized_column_sq_le line 126

Source documentation

Squared row errors remain squared after passage to every covector.

theorem normalized_column_sq_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (Ω : Set X) (hfin : μ Ω ≠ ∞) {E : ℝ} (hE : 0 ≤ E)
    (hrow : ∀ j, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (u j))‖ ^ 2 ≤ E)
    (b : Euclidean n) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (sobolevColumnMap μ hQ u b))‖ ^ 2 ≤
      (n : ℝ) ^ 2 * E * ‖b‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap