RankMeasure.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional rank bookkeeping

The differentiation--multiplication measure is obtained by applying a linear family of linear maps to a polynomial. Its rank can be studied independently of the construction of that family and the choice of homogeneous spaces.

def OAI.Problem335.RankMeasure.mapRank line 30
Source documentation
The natural-number rank of a linear map. Its use below always has a finite-dimensional source, or an explicit finite-dimensional factorization.
```
def mapRank (f : V →ₗ[K] W) : ℕ := Module.finrank K (LinearMap.range f)
```
theorem OAI.Problem335.RankMeasure.mapRank_zero line 32
theorem OAI.Problem335.RankMeasure.mapRank_smul line 35
theorem OAI.Problem335.RankMeasure.mapRank_smul_le line 40
theorem OAI.Problem335.RankMeasure.mapRank_add_le line 44
theorem OAI.Problem335.RankMeasure.mapRank_sum_le line 52
theorem OAI.Problem335.RankMeasure.mapRank_comp_le_left line 62
theorem OAI.Problem335.RankMeasure.mapRank_comp_le_right line 69
theorem OAI.Problem335.RankMeasure.mapRank_factor_le line 77
Source documentation
Factorization through a finite-dimensional intermediate space bounds rank.
```
theorem mapRank_factor_le [FiniteDimensional K Z]
    (f : V →ₗ[K] Z) (g : Z →ₗ[K] W) :
    mapRank (g.comp f) ≤ Module.finrank K Z :=
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank

theorem OAI.Problem335.RankMeasure.mapRank_eq_matrixRank line 83

Source documentation

Changing to finite bases identifies our rank convention with matrix rank.

theorem mapRank_eq_matrixRank {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq ι] [DecidableEq κ]
    (bV : Module.Basis ι K V) (bW : Module.Basis κ K W) (f : V →ₗ[K] W) :
    mapRank f = (LinearMap.toMatrix bV bW f).rank := by
…

Mentions: OAI.Problem335.RankMeasure.mapRank

theorem OAI.Problem335.RankMeasure.mapRank_subtype_comp line 94
Source documentation
The rank of a restricted map does not depend on whether its codomain is viewed as a subspace or as the ambient space.
```
theorem mapRank_subtype_comp (S : Submodule K W) (f : V →ₗ[K] S) :
    mapRank (S.subtype.comp f) = mapRank f := by
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank
def OAI.Problem335.RankMeasure.restrictFamily line 103
Source documentation
Restrict the source of a linear operator family to a chosen homogeneous subspace, leaving the codomain ambient. This avoids unnecessary transports between equivalent descriptions of the target homogeneous space.
```
def restrictFamily (F : P →ₗ[K] (V →ₗ[K] W)) (S : Submodule K V) :
    P →ₗ[K] (S →ₗ[K] W) where
…
```
theorem OAI.Problem335.RankMeasure.restrictFamily_apply line 109
theorem OAI.Problem335.RankMeasure.mapRank_restrict_factor_le line 115
Source documentation
In a product of operators, it suffices to show that the first part sends the source subspace into a finite-dimensional intermediate subspace.
```
theorem mapRank_restrict_factor_le (S : Submodule K V) (I : Submodule K Z)
    [FiniteDimensional K I] (f : V →ₗ[K] Z) (g : Z →ₗ[K] W)
    (hf : ∀ x : S, f x ∈ I) :
    mapRank ((g.comp f).comp S.subtype) ≤ Module.finrank K I := by
…
```
Mentions: OAI.Problem335.RankMeasure.mapRank
def OAI.Problem335.RankMeasure.measure line 127
Source documentation
A rank measure associated with a linear family of linear maps.
```
def measure (F : P →ₗ[K] (V →ₗ[K] W)) (p : P) : ℕ := mapRank (F p)
```
Mentions: OAI.Problem335.RankMeasure.mapRank
theorem OAI.Problem335.RankMeasure.measure_zero line 129
theorem OAI.Problem335.RankMeasure.measure_smul line 133
theorem OAI.Problem335.RankMeasure.measure_smul_le line 137
theorem OAI.Problem335.RankMeasure.measure_add_le line 142
theorem OAI.Problem335.RankMeasure.measure_sum_le line 147

theorem OAI.Problem335.RankMeasure.measure_sum_smul_le line 153

Source documentation

Scalar coefficients introduce no extra rank cost, including zero coefficients.

theorem measure_sum_smul_le [FiniteDimensional K V] {ι : Type*}
    (F : P →ₗ[K] (V →ₗ[K] W)) (s : Finset ι) (a : ι → K) (p : ι → P) :
    measure F (∑ i ∈ s, a i • p i) ≤ ∑ i ∈ s, measure F (p i) := by
…

Mentions: OAI.Problem335.RankMeasure.measure

theorem OAI.Problem335.RankMeasure.measure_sum_smul_le_card_mul line 161

Source documentation

A sum of at most s.card contributions of rank at most B has rank at most s.card * B. This is the gate-counting step for additive layers.

theorem measure_sum_smul_le_card_mul [FiniteDimensional K V] {ι : Type*}
    (F : P →ₗ[K] (V →ₗ[K] W)) (s : Finset ι) (a : ι → K) (p : ι → P)
    (B : ℕ) (hB : ∀ i ∈ s, measure F (p i) ≤ B) :
    measure F (∑ i ∈ s, a i • p i) ≤ s.card * B := by
…

Mentions: OAI.Problem335.RankMeasure.measure

theorem OAI.Problem335.RankMeasure.mapRank_sum_factor_le line 170

Source documentation

Each summand may factor through its own finite-dimensional intermediate space, as occurs when bidegrees of the factors are fixed separately.

theorem mapRank_sum_factor_le [FiniteDimensional K V] {ι : Type*}
    {Z' : ι → Type y} [∀ i, AddCommGroup (Z' i)] [∀ i, Module K (Z' i)]
    [∀ i, FiniteDimensional K (Z' i)] (s : Finset ι)
    (f : ∀ i, V →ₗ[K] Z' i) (g : ∀ i, Z' i →ₗ[K] W) :
    mapRank (∑ i ∈ s, (g i).comp (f i)) ≤
      ∑ i ∈ s, Module.finrank K (Z' i) := by
…

Mentions: OAI.Problem335.RankMeasure.mapRank

theorem OAI.Problem335.RankMeasure.measure_le_sum_of_factorizations line 179