WeightedGrading.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

The actual weighted orthogonal grading of the cube

The construction first orthogonalizes an arbitrary finite flag of subspaces. It then transports the concrete Walsh flag by the invertible square-root weight and takes the orthogonal projections in the counting Hilbert space. The resulting matrices are proved to form an orthogonal decomposition of the identity with the prescribed binomial multiplicities.

def OAI.LeanBlast.GotsmanLinial.flagLayer line 36
Source documentation
The new orthogonal layer appearing between two consecutive stages of a flag.
```
def flagLayer (K : ℕ → Submodule 𝕜 E) (k : ℕ) : Submodule 𝕜 E :=
…
```
def OAI.LeanBlast.GotsmanLinial.flagProjection line 40
Source documentation
The actual orthogonal projection onto a layer of a finite-dimensional flag.
```
def flagProjection (K : ℕ → Submodule 𝕜 E) (k : ℕ) : E →L[𝕜] E :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_le_next line 44
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_le_prev_orthogonal line 48
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_sup_prev line 51
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_finrank_add line 56
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_finrank line 62
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_isOrtho_of_lt line 68
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_isOrtho line 75
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_iSup_eq_top line 81
theorem OAI.LeanBlast.GotsmanLinial.flagLayer_orthogonalFamily line 99
theorem OAI.LeanBlast.GotsmanLinial.flagProjection_isSelfAdjoint line 107
theorem OAI.LeanBlast.GotsmanLinial.flagProjection_idempotent line 111
theorem OAI.LeanBlast.GotsmanLinial.flagProjection_mul_eq_zero line 115
theorem OAI.LeanBlast.GotsmanLinial.sum_flagProjection line 119
theorem OAI.LeanBlast.GotsmanLinial.range_flagProjection line 130
theorem OAI.LeanBlast.GotsmanLinial.flagProjection_apply_mem_next line 134
theorem OAI.LeanBlast.GotsmanLinial.flagProjection_apply_eq_zero_of_mem_prev line 138
def OAI.LeanBlast.GotsmanLinial.coordinateMulEquiv line 153
Source documentation
Multiplication by pointwise nonzero coefficients is a linear equivalence.
```
def coordinateMulEquiv (a : Ω → ℂ) (ha : ∀ x, a x ≠ 0) :
    (Ω → ℂ) ≃ₗ[ℂ] (Ω → ℂ) where
…
```
def OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv line 172
Source documentation
Multiplication by the square root of a strictly positive weight, in the counting Euclidean Hilbert space.
```
def sqrtWeightEquiv (w : Ω → ℝ) (hw : ∀ x, 0 < w x) :
    EuclideanSpace ℂ Ω ≃ₗ[ℂ] EuclideanSpace ℂ Ω :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv_apply line 181
theorem OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv_symm_apply line 187
def OAI.LeanBlast.GotsmanLinial.transportFlag line 199
Source documentation
Transport a degree flag through an invertible linear weight operator.
```
def transportFlag (D : E ≃ₗ[𝕜] E) (F : ℕ → Submodule 𝕜 E) (k : ℕ) :
    Submodule 𝕜 E := (F k).map D.toLinearMap
```
theorem OAI.LeanBlast.GotsmanLinial.transportFlag_monotone line 202
theorem OAI.LeanBlast.GotsmanLinial.transportFlag_zero line 207
theorem OAI.LeanBlast.GotsmanLinial.transportFlag_top line 211
theorem OAI.LeanBlast.GotsmanLinial.transportFlag_finrank line 215

theorem OAI.LeanBlast.GotsmanLinial.transportFlag_layer_finrank line 220

Source documentation

The weighted construction preserves every prescribed dimension increment.

theorem transportFlag_layer_finrank [FiniteDimensional 𝕜 E] (D : E ≃ₗ[𝕜] E)
    (F : ℕ → Submodule 𝕜 E) (hF : Monotone F) (k d : ℕ)
    (hd : finrank 𝕜 (F k) + d = finrank 𝕜 (F (k + 1))) :
    finrank 𝕜 (flagLayer (transportFlag D F) k) = d := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.flagLayer, OAI.LeanBlast.GotsmanLinial.transportFlag

def OAI.LeanBlast.GotsmanLinial.flagProjectionMatrix line 238
Source documentation
Matrix of an actual flag-layer projection in an orthonormal basis.
```
def flagProjectionMatrix (b : OrthonormalBasis ι ℂ E)
    (K : ℕ → Submodule ℂ E) (k : ℕ) : Matrix ι ι ℂ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.flagProjectionMatrix_family line 244
Source documentation
The matrix projection-family laws follow from the constructed Hilbert-space projections, without any additional grading hypothesis.
```
theorem flagProjectionMatrix_family (b : OrthonormalBasis ι ℂ E)
    (K : ℕ → Submodule ℂ E) (hK : Monotone K) (hzero : K 0 = ⊥)
    (n : ℕ) (htop : K (n + 1) = ⊤) :
    OrthogonalProjectionFamily (fun k : Fin (n + 1) => flagProjectionMatrix b K k.val) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.flagProjectionMatrix
theorem OAI.LeanBlast.GotsmanLinial.trace_flagProjectionMatrix line 255
theorem OAI.LeanBlast.GotsmanLinial.re_trace_flagProjectionMatrix line 260
def OAI.LeanBlast.GotsmanLinial.weightedFourierSpace line 272
Source documentation
The weighted degree-k subspace of the counting Hilbert space.
```
def weightedFourierSpace (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) (k : ℕ) :
    Submodule ℂ (EuclideanSpace ℂ (Cube n)) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.weightedFourierFlag line 277
Source documentation
The weighted Fourier flag, shifted by one so that stage zero is bottom.
```
def weightedFourierFlag (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) :
    ℕ → Submodule ℂ (EuclideanSpace ℂ (Cube n)) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.weightedFourierFlag_zero line 282
theorem OAI.LeanBlast.GotsmanLinial.weightedFourierFlag_succ line 287
theorem OAI.LeanBlast.GotsmanLinial.weightedFourierFlag_mono line 290
theorem OAI.LeanBlast.GotsmanLinial.weightedFourierFlag_top line 295
theorem OAI.LeanBlast.GotsmanLinial.weightedFourierFlag_layer_finrank line 300
Source documentation
Weighting preserves the exact binomial dimensions of the orthogonal layers.
```
theorem weightedFourierFlag_layer_finrank (w : Cube n → ℝ) (hw : ∀ x, 0 < w x)
    (k : ℕ) :
    finrank ℂ (flagLayer (weightedFourierFlag w hw) k) = n.choose k :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.flagLayer, OAI.LeanBlast.GotsmanLinial.weightedFourierFlag
def OAI.LeanBlast.GotsmanLinial.weightedProjection line 307
Source documentation
Actual orthogonal projection onto weighted Fourier layer k.
```
def weightedProjection (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) (k : Fin (n + 1)) :
    EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix line 312
Source documentation
The projection represented in the point-mass orthonormal basis.
```
def weightedProjectionMatrix (w : Cube n → ℝ) (hw : ∀ x, 0 < w x)
    (k : Fin (n + 1)) : Matrix (Cube n) (Cube n) ℂ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.weightedProjection_apply_mem line 317
theorem OAI.LeanBlast.GotsmanLinial.weightedProjection_annihilate_prev line 322
theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_family line 327
theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_trace line 333
theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_trace_re line 338
theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_hsNormSq line 344
theorem OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv_commute_signMultiplier line 351
Source documentation
Every real diagonal multiplier commutes with the positive square-root weight.
```
theorem sqrtWeightEquiv_commute_signMultiplier
    (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) (h : Cube n → ℝ)
    (f : EuclideanSpace ℂ (Cube n)) :
    signMultiplier h (sqrtWeightEquiv w hw f) =
      sqrtWeightEquiv w hw (signMultiplier h f) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.signMultiplier, OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv
theorem OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv_commute_coordinateMultiplier line 360