HarmonicGrams.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Gram operators of Sobolev coordinate columns

These operators use the canonical carré du champ of the Cheeger energy. The change-of-coordinates formula is therefore an identity for the actual energy, rather than an assumption about an auxiliary matrix field.

def OAI.RegularPointCoordinates.sobolevColumnMap line 26
Source documentation
Linear combinations of the scalar coordinate functions.
```
def sobolevColumnMap {n : ℕ} (u : Fin n → SobolevSpace μ hQ) :
    Euclidean n →L[ℝ] SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.sobolevColumnMap_apply line 31
theorem OAI.RegularPointCoordinates.sobolevColumnMap_single line 36
def OAI.RegularPointCoordinates.sobolevGramForm line 47
Source documentation
The weighted mean energy as a continuous symmetric bilinear form.
```
def sobolevGramForm : E →L[ℝ] E →L[ℝ] ℝ :=
…
```
theorem OAI.RegularPointCoordinates.sobolevGramForm_apply line 51
def OAI.RegularPointCoordinates.sobolevGram line 56
Source documentation
Riesz representation of the weighted Sobolev Gram form.
```
def sobolevGram : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.sobolevGram_inner line 59
theorem OAI.RegularPointCoordinates.sobolevGram_energy line 64
theorem OAI.RegularPointCoordinates.sobolevGram_isSymmetric line 69
theorem OAI.RegularPointCoordinates.sobolevGram_isPositive line 78
theorem OAI.RegularPointCoordinates.sobolevGram_comp line 88
Source documentation
Changing the coordinate columns conjugates their actual Gram operator.
```
theorem sobolevGram_comp (A : E →L[ℝ] E) :
    sobolevGram μ hQ (U.comp A) hw hb =
      A.adjoint.comp ((sobolevGram μ hQ U hw hb).comp A) := by
…
```
Mentions: OAI.RegularPointCoordinates.sobolevGram

theorem OAI.RegularPointCoordinates.sobolevGram_energy_mono line 100

Source documentation

Pointwise comparison of weights gives comparison of every Gram energy.

theorem sobolevGram_energy_mono {w' : X → ℝ}
    (hw' : AEStronglyMeasurable w' μ) {C' : ℝ≥0}
    (hb' : ∀ᵐ x ∂μ, ‖w' x‖ ≤ (C' : ℝ))
    (hle : ∀ᵐ x ∂μ, w x ≤ w' x) (v : E) :
    ⟪v, sobolevGram μ hQ U hw hb v⟫_ℝ ≤
      ⟪v, sobolevGram μ hQ U hw' hb' v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.sobolevGram

def OAI.RegularPointCoordinates.sobolevMeanGram line 120
Source documentation
The Gram average on a measurable set, with its actual reference measure.
```
def sobolevMeanGram (s : Set X) (hs : MeasurableSet s) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.sobolevMeanGram_energy line 127
theorem OAI.RegularPointCoordinates.sobolevMeanGram_inner line 139
theorem OAI.RegularPointCoordinates.sobolevMeanGram_column_entry line 150
theorem OAI.RegularPointCoordinates.sobolevMeanGram_isPositive line 157
theorem OAI.RegularPointCoordinates.sobolevMeanGram_comp line 165
def OAI.RegularPointCoordinates.IsSobolevHarmonicOn line 182
Source documentation
Local harmonicity is tested against the existing zero-boundary Sobolev space, using the canonical Dirichlet energy.
```
def IsSobolevHarmonicOn (Ω : Set X) (f : SobolevSpace μ hQ) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.add line 187
theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.smul line 194
theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.linearCombination line 201