MatrixNormalization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.rank_diagonal_mul_mul_diagonal line 17

Source documentation

Nonzero row and column rescalings preserve the rank of a rectangular matrix.

theorem rank_diagonal_mul_mul_diagonal (A : Matrix κ ι K)
    (r : κ → K) (c : ι → K) (hr : ∀ i, r i ≠ 0) (hc : ∀ j, c j ≠ 0) :
    (Matrix.diagonal r * A * Matrix.diagonal c).rank = A.rank := by
…

theorem OAI.Problem335.rank_entrywise_scaling line 30

Source documentation

Entrywise nonzero row/column normalization does not change rank.

theorem rank_entrywise_scaling (A : Matrix κ ι K)
    (r : κ → K) (c : ι → K) (hr : ∀ i, r i ≠ 0) (hc : ∀ j, c j ≠ 0) :
    Matrix.rank (fun i j => r i * A i j * c j : Matrix κ ι K) = A.rank := by
…

theorem OAI.Problem335.toMatrix_unitsSMul_apply line 50

Source documentation

Rescaling source and target basis vectors rescales matrix columns and rows, with inverse target weights. This identifies normalized-monomial matrices.

theorem toMatrix_unitsSMul_apply (f : M →ₗ[K] N)
    (b : Module.Basis ι K M) (c : Module.Basis κ K N)
    (u : ι → Kˣ) (v : κ → Kˣ) (i : κ) (j : ι) :
    LinearMap.toMatrix (b.unitsSMul u) (c.unitsSMul v) f i j =
      (↑((v i)⁻¹) : K) * LinearMap.toMatrix b c f i j * (u j : K) := by
…

theorem OAI.Problem335.rank_sqrt_normalization line 62

Source documentation

The square-root rescaling used by factorial-normalized monomial bases preserves rank whenever all normalization weights are positive.

theorem rank_sqrt_normalization {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq ι] [DecidableEq κ] (A : Matrix κ ι ℂ)
    (r : κ → ℝ) (c : ι → ℝ) (hr : ∀ i, 0 < r i) (hc : ∀ j, 0 < c j) :
    Matrix.rank (fun i j => (Real.sqrt (r i) : ℂ) * A i j /
      (Real.sqrt (c j) : ℂ)) = A.rank := by
…

theorem OAI.Problem335.rank_lower_bound_of_trace_moment_bounds line 80

Source documentation

Comparing the first two normalized trace moments gives the rank bound used in the IMM argument. Here w contains the path count and local moment factor.

theorem rank_lower_bound_of_trace_moment_bounds (A : Matrix κ ι ℂ)
    {D w δ ε : ℝ} (hD : 0 < D) (hw : 0 < w)
    (hfirst : D * w * Real.exp (-δ) ≤ (Aᴴ * A).trace.re)
    (hsecond : (((Aᴴ * A) ^ 2).trace.re) ≤ D * w ^ 2 * Real.exp ε) :
    D * Real.exp (-(2 * δ + ε)) ≤ (A.rank : ℝ) := by
…