Problem 1.4: Sub-Gaussian random matrices

noncomputable def Problem_1_4.matrixOpNorm {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℝ) : ℝ

theorem Problem_1_4.problem_1_4a_matrix_subgaussian {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (x✝¹ : MeasureTheory.IsProbabilityMeasure μ) {n m : ℕ} {A : Ω → Matrix (Fin n) (Fin m) ℝ} {σsq : ℝ} (hSG : ∀ (i : Fin n) (j : Fin m), IsSubGaussian (fun (ω : Ω) => A ω i j) σsq μ) (hIndep : ProbabilityTheory.iIndepFun (fun (p : Fin n × Fin m) (ω : Ω) => A ω p.1 p.2) μ) (x : EuclideanSpace ℝ (Fin m)) (y : EuclideanSpace ℝ (Fin n)) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : IsSubGaussian (fun (ω : Ω) => inner ℝ ((Matrix.toEuclideanLin (A ω)) x) y) σsq μ

Problem 1.4 (a)

theorem Problem_1_4.integral_exp_sub_one_sub {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (f ω)) μ) (hmean : ∫ (ω : Ω), f ω ∂μ = 0) : ∫ (ω : Ω), Real.exp (f ω) - 1 - f ω ∂μ = ∫ (ω : Ω), Real.exp (f ω) ∂μ - 1

Helper: integral of exp(f) - 1 - f equals E[exp(f)] - 1 when E[f] = 0.

theorem Problem_1_4.subgaussian_zero_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hSG : IsSubGaussian X 0 μ) : X =ᵐ[μ] 0

If X is sub-Gaussian with σ² = 0, then X = 0 a.e. Proof: E[exp(sX)] ≤ 1 for all s. By Jensen, E[exp(X)] ≥ exp(E[X]) = 1. So E[exp(X)] = 1. Since exp(x) ≥ 1 + x with equality iff x = 0, the function g(ω) = exp(X(ω)) - 1 - X(ω) is nonneg with integral 0, hence 0 a.e. This forces X = 0 a.e.

theorem Problem_1_4.problem_1_4b_operator_norm_bound {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (x✝¹ : MeasureTheory.IsProbabilityMeasure μ) {n m : ℕ} {A : Ω → Matrix (Fin n) (Fin m) ℝ} {σsq : ℝ} (hσsq : 0 ≤ σsq) (hSG : ∀ (i : Fin n) (j : Fin m), IsSubGaussian (fun (ω : Ω) => A ω i j) σsq μ) (hIndep : ProbabilityTheory.iIndepFun (fun (p : Fin n × Fin m) (ω : Ω) => A ω p.1 p.2) μ) (hMeas : ∀ (i : Fin n) (j : Fin m), Measurable fun (ω : Ω) => A ω i j) : ∃ (C : ℝ), 0 < C ∧ ∫ (ω : Ω), matrixOpNorm (A ω) ∂μ ≤ C * √σsq * (√↑m + √↑n)

Problem 1.4 (b)