Orthogonality.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DiamondDistortion.SegmentSystem.primal_sq_le line 16
def OAI.DiamondDistortion.SegmentSystem.colorSupport line 32

lemma OAI.DiamondDistortion.SegmentSystem.block_add_sq line 35

Source documentation

Segment families in disjoint components spend orthogonal testing energies.

lemma block_add_sq (c : ι → κ)
    (hsame : ∀ S, T.IsSegment S → ∀ u ∈ S, ∀ v ∈ S, c u=c v)
    (p q : ι →₀ ℝ) (hd : Disjoint (T.colorSupport c p) (T.colorSupport c q)) :
    (T.primalSeminorm (p+q))^2 ≤ (T.primalSeminorm p)^2+(T.primalSeminorm q)^2 := by
…

lemma OAI.DiamondDistortion.SegmentSystem.small_color_tail_upper line 65

Source documentation

A functional on an orthogonal sum is uniformly small outside finitely many components. The proof uses finite blocks only, not a reflexivity library.

lemma small_color_tail_upper (c : ι → κ)
    (hsame : ∀ S, T.IsSegment S → ∀ u ∈ S, ∀ v ∈ S, c u=c v)
    (x : T.Dual) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : Finset κ, ∀ p : ι →₀ ℝ, (∀ v ∈ p.support, c v ∉ C) →
      x (T.finiteEmbedding p) ≤ ε*T.primalSeminorm p := by
…

lemma OAI.DiamondDistortion.SegmentSystem.small_color_tail line 131
lemma OAI.DiamondDistortion.SegmentSystem.sum_sq_le_support line 146
Source documentation
No nonzero coordinate is lost by using the actual Finsupp support.
```
lemma sum_sq_le_support (p : ι →₀ ℝ) (S : Finset ι) :
    (∑ v ∈ S,p v^2) ≤ ∑ v ∈ p.support,p v^2 := by
…
```
lemma OAI.DiamondDistortion.SegmentSystem.coordinate_energy_le line 158
lemma OAI.DiamondDistortion.SegmentSystem.primal_sq_le_of_segment line 170
def OAI.DiamondDistortion.SegmentSystem.finiteArray line 186
lemma OAI.DiamondDistortion.SegmentSystem.finiteArray_apply line 189
lemma OAI.DiamondDistortion.SegmentSystem.finiteArray_support line 194
lemma OAI.DiamondDistortion.SegmentSystem.finiteArray_energy line 199
lemma OAI.DiamondDistortion.SegmentSystem.finiteArray_pairing line 212
lemma OAI.DiamondDistortion.SegmentSystem.finite_square_tails line 218
Source documentation
Bounded nonnegative finite square sums have uniformly small disjoint tails. This is proved directly from a real supremum, with no countability assumption.
```
lemma finite_square_tails (a : ι → ℝ) {M : ℝ}
    (hM : ∀ S : Finset ι,(∑ v ∈ S,a v^2) ≤ M) {δ : ℝ} (hδ : 0 < δ) :
    ∃ S : Finset ι, ∀ U : Finset ι, Disjoint S U → (∑ v ∈ U,a v^2) < δ := by
…
```