Documentation

HighDimProb.RandomMatrix.Basic

Basic random matrix vocabulary #

Verified Wikipedia reference:

source
@[implicit_reducible]
instance HighDimProb.instMeasurableSpaceMatrix {m : Type u_1} {n : Type u_2} {alpha : Type u_3} [MeasurableSpace alpha] :
MeasurableSpace (Matrix m n alpha)

Product measurable-space structure for finite matrices.

Formula reference: a random matrix is a matrix-valued random object; the product measurable-space instance supplies the measurable side of that vocabulary. See https://en.wikipedia.org/wiki/Random_matrix

source
@[reducible, inline]
abbrev HighDimProb.RandomMatrix (Omega : Type u_1) [MeasurableSpace Omega] (m n : ℕ) :
Type u_1

An m x n real random matrix with concrete finite dimensions.

Formula reference: this is the Lean type for a finite-dimensional random matrix; see https://en.wikipedia.org/wiki/Random_matrix

Instances For
    source
    def HighDimProb.matrixEntry {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (A : RandomMatrix Omega m n) (i : Fin m) (j : Fin n) :
    RealRandomVariable Omega

    Entry random variable of a random matrix.

    Formula reference: matrix-valued randomness is checked entrywise here; see https://en.wikipedia.org/wiki/Random_matrix

    Instances For
      source
      @[reducible, inline]
      abbrev HighDimProb.IsRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (P : MeasureTheory.Measure Omega) (A : RandomMatrix Omega m n) :
      Prop

      Entrywise measurability predicate for random matrices.

      Formula reference: this predicate records that each matrix entry is a real random variable, matching the entrywise view of a random matrix; see https://en.wikipedia.org/wiki/Random_matrix

      Instances For
        source
        @[simp]
        theorem HighDimProb.matrixEntry_apply {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (A : RandomMatrix Omega m n) (i : Fin m) (j : Fin n) (omega : Omega) :
        matrixEntry A i j omega = A omega i j

        Formula reference: this unfolds the entry random variable A_ij; see https://en.wikipedia.org/wiki/Random_matrix

        source
        def HighDimProb.scaledRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (theta : ℝ) (A : RandomMatrix Omega m n) :
        RandomMatrix Omega m n

        Pointwise scalar multiple of a random matrix.

        This names the object-level adapter so theorem statements can refer to a scaled random matrix without exposing an anonymous lambda.

        Instances For
          source
          def HighDimProb.scaledRandomMatrixFamily {Omega : Type u_1} [MeasurableSpace Omega] {I : Type u_2} {m n : ℕ} (theta : ℝ) (A : I → RandomMatrix Omega m n) :
          I → RandomMatrix Omega m n

          Indexed family of pointwise scalar multiples of random matrices.

          This is the family-level adapter used by trace-MGF and Matrix Bernstein routes when a finite family is rescaled by a scalar parameter.

          Instances For
            source
            def HighDimProb.negRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (A : RandomMatrix Omega m n) :
            RandomMatrix Omega m n

            Pointwise negation of a random matrix.

            This names the object-level negative adapter so public theorem statements can refer to a negated random matrix without exposing an anonymous lambda.

            Instances For
              source
              @[simp]
              theorem HighDimProb.scaledRandomMatrix_apply {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (theta : ℝ) (A : RandomMatrix Omega m n) (omega : Omega) :
              scaledRandomMatrix theta A omega = SMul.smul theta (A omega)
              source
              @[simp]
              theorem HighDimProb.scaledRandomMatrixFamily_apply {Omega : Type u_1} [MeasurableSpace Omega] {I : Type u_2} {m n : ℕ} (theta : ℝ) (A : I → RandomMatrix Omega m n) (i : I) :
              scaledRandomMatrixFamily theta A i = scaledRandomMatrix theta (A i)
              source
              @[simp]
              theorem HighDimProb.scaledRandomMatrixFamily_apply_apply {Omega : Type u_1} [MeasurableSpace Omega] {I : Type u_2} {m n : ℕ} (theta : ℝ) (A : I → RandomMatrix Omega m n) (i : I) (omega : Omega) :
              scaledRandomMatrixFamily theta A i omega = SMul.smul theta (A i omega)
              source
              @[simp]
              theorem HighDimProb.negRandomMatrix_apply {Omega : Type u_1} [MeasurableSpace Omega] {m n : ℕ} (A : RandomMatrix Omega m n) (omega : Omega) :
              negRandomMatrix A omega = -A omega
              source
              theorem HighDimProb.isRandomMatrix_scaledRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {m n : ℕ} {A : RandomMatrix Omega m n} (theta : ℝ) (hA : IsRandomMatrix P A) :
              IsRandomMatrix P (scaledRandomMatrix theta A)

              Pointwise scalar multiplication preserves entrywise random-matrix measurability.

              source
              theorem HighDimProb.isRandomMatrix_scaledRandomMatrixFamily {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {I : Type u_2} {m n : ℕ} {A : I → RandomMatrix Omega m n} (theta : ℝ) (hA : ∀ (i : I), IsRandomMatrix P (A i)) (i : I) :
              IsRandomMatrix P (scaledRandomMatrixFamily theta A i)

              Pointwise scalar multiplication preserves entrywise random-matrix measurability for indexed families.

              source
              theorem HighDimProb.isRandomMatrix_negRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {m n : ℕ} {A : RandomMatrix Omega m n} (hA : IsRandomMatrix P A) :
              IsRandomMatrix P (negRandomMatrix A)

              Pointwise negation preserves entrywise random-matrix measurability.

              source
              def HighDimProb.rankOneMatrix {n : ℕ} (x : Fin n → ℝ) :
              Matrix (Fin n) (Fin n) ℝ

              Deterministic rank-one self outer-product matrix associated to a vector.

              Formula reference: the outer product has entries x_i * x_j; see https://en.wikipedia.org/wiki/Outer_product .

              Instances For
                source
                @[simp]
                theorem HighDimProb.rankOneMatrix_apply {n : ℕ} (x : Fin n → ℝ) (i j : Fin n) :
                rankOneMatrix x i j = x i * x j

                Formula reference: this unfolds the rank-one outer-product entry x_i * x_j; see https://en.wikipedia.org/wiki/Outer_product .

                source
                def HighDimProb.rankOneRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {n : ℕ} (X : RandomVector Omega n) :
                RandomMatrix Omega n n

                Rank-one self outer-product random matrix associated to a random vector.

                Formula reference: the outer product has entries x_i * x_j; see https://en.wikipedia.org/wiki/Outer_product . This declaration only exposes the object-level vector-to-matrix map; measurability and integrability remain separate assumptions/bridges, matching the random-vector convention at https://en.wikipedia.org/wiki/Random_vector .

                Instances For
                  source
                  def HighDimProb.rankOneRandomMatrixFamily {Omega : Type u_1} [MeasurableSpace Omega] {I : Type u_2} {n : ℕ} (X : I → RandomVector Omega n) :
                  I → RandomMatrix Omega n n

                  Indexed family of rank-one self outer-product random matrices.

                  This names the family-level adapter so downstream APIs can refer to the rank-one matrix family directly.

                  Instances For
                    source
                    @[simp]
                    theorem HighDimProb.rankOneRandomMatrix_apply {Omega : Type u_1} [MeasurableSpace Omega] {n : ℕ} (X : RandomVector Omega n) (omega : Omega) (i j : Fin n) :
                    rankOneRandomMatrix X omega i j = X omega i * X omega j

                    Formula reference: this unfolds the rank-one outer-product entry X_i(omega) * X_j(omega); see https://en.wikipedia.org/wiki/Outer_product .

                    source
                    @[simp]
                    theorem HighDimProb.rankOneRandomMatrixFamily_apply {Omega : Type u_1} [MeasurableSpace Omega] {I : Type u_2} {n : ℕ} (X : I → RandomVector Omega n) (i : I) :
                    rankOneRandomMatrixFamily X i = rankOneRandomMatrix (X i)
                    source
                    @[simp]
                    theorem HighDimProb.matrixEntry_rankOneRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {n : ℕ} (X : RandomVector Omega n) (i j : Fin n) (omega : Omega) :
                    matrixEntry (rankOneRandomMatrix X) i j omega = X omega i * X omega j

                    Formula reference: the matrix entry of a rank-one outer product is the product of the corresponding vector coordinates; see https://en.wikipedia.org/wiki/Outer_product .

                    source
                    theorem HighDimProb.isRealRandomVariable_matrixEntry {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {m n : ℕ} {A : RandomMatrix Omega m n} (hA : IsRandomMatrix P A) (i : Fin m) (j : Fin n) :
                    IsRealRandomVariable P (matrixEntry A i j)

                    Entries of an IsRandomMatrix are real random variables.

                    Formula reference: entrywise random-variable structure is the finite-matrix specialization of random matrices; see https://en.wikipedia.org/wiki/Random_matrix

                    source
                    theorem HighDimProb.isRandomMatrix_rankOneRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n : ℕ} {X : RandomVector Omega n} (hX : IsRandomVector P X) :
                    IsRandomMatrix P (rankOneRandomMatrix X)

                    Rank-one self outer products of random vectors are random matrices.

                    Formula reference: each entry is the product X_i * X_j; measurability follows from closure of measurable real functions under multiplication. See https://en.wikipedia.org/wiki/Outer_product and https://en.wikipedia.org/wiki/Measurable_function .

                    source
                    theorem HighDimProb.measurable_randomMatrix_of_isRandomMatrix {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {m n : ℕ} {A : RandomMatrix Omega m n} (hA : IsRandomMatrix P A) :
                    Measurable A

                    Entrywise measurability gives measurability of the matrix-valued map.

                    Formula reference: this upgrades entrywise measurable random variables to a matrix-valued random object; see https://en.wikipedia.org/wiki/Random_matrix

                    source
                    theorem HighDimProb.isRandomMatrix_of_sub_measurable_entries {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {m n : ℕ} {A : RandomMatrix Omega m n} (mSub : MeasurableSpace Omega) (hSub : mSub ≤ mOmega) (hA : ∀ (i : Fin m) (j : Fin n), Measurable fun (omega : Omega) => A omega i j) :
                    IsRandomMatrix P A

                    Entrywise measurability in a smaller measurable space gives ambient random-matrix measurability when the smaller space is below the ambient one.