noncomputable def chapter03Example333ReportedBetaSq : ℝ

Chapter03 Example 3.3.3 (1): the reported value of β² is 1.061.

@[simp]

theorem chapter03Example333ReportedBetaSq_def : chapter03Example333ReportedBetaSq = 1061 / 1000

The reported constant β² is the rational value 1061 / 1000.

noncomputable def chapter03Example333InputMatrix : Matrix (Fin 3) (Fin 3) ℝ

Chapter03 Example 3.3.3 (2): the concrete matrix G_k from formula (3.3.15).

noncomputable def chapter03Example333ReportedL : Matrix (Fin 3) (Fin 3) ℝ

The lower-triangular factor L reported in Example 3.3.3.

noncomputable def chapter03Example333ReportedD : Matrix (Fin 3) (Fin 3) ℝ

The diagonal matrix D reported in Example 3.3.3.

noncomputable def chapter03Example333ReportedE : Matrix (Fin 3) (Fin 3) ℝ

The diagonal correction matrix E_k reported in Example 3.3.3.

noncomputable def chapter03Example333ReportedCorrectedMatrix : Matrix (Fin 3) (Fin 3) ℝ

The corrected matrix Ḡ_k = G_k + E_k attached to the reported data of Example 3.3.3.

@[simp]

theorem chapter03Example333ReportedCorrectedMatrix_sub_inputMatrix : chapter03Example333ReportedCorrectedMatrix - chapter03Example333InputMatrix = chapter03Example333ReportedE

The concrete correction satisfies Ḡ_k - G_k = E_k.

theorem chapter03Example333_reportedCorrectionFrobeniusNorm_eq : ‖chapter03Example333ReportedCorrectedMatrix - chapter03Example333InputMatrix‖_F = ‖chapter03Example333ReportedE‖_F

Chapter03 Example 3.3.3 (3): for the reported correction matrix, ‖Ḡ_k - G_k‖_F = ‖E_k‖_F.

theorem chapter03Example333_reportedCorrectionFrobeniusNorm_sq : ‖chapter03Example333ReportedE‖_F ^ 2 = 37869746 / 1000000

Helper for Chapter03 Example 3.3.3: the squared Frobenius norm of the reported diagonal correction has the exact rational value coming from its three diagonal entries.

theorem chapter03Example333_reportedCorrectionFrobeniusNorm_rounded : |‖chapter03Example333ReportedCorrectedMatrix - chapter03Example333InputMatrix‖_F - 6154 / 1000| ≤ 1 / 2000

Chapter03 Example 3.3.3 (4): the Frobenius norm of the concrete correction Ḡ_k - G_k is reported by the rounded value 6154 / 1000 = 6.154.

noncomputable def chapter03Example333ReportedCorrectedMatrixCore : Matrix (Fin 3) (Fin 3) ℝ

Helper for Chapter03 Example 3.3.3: the rational core of the corrected matrix keeps the reported rounded entries and drops only the tiny 10^-20 diagonal perturbation.

noncomputable def chapter03Example333ReportedTinyDiagonalCorrection : Matrix (Fin 3) (Fin 3) ℝ

Helper for Chapter03 Example 3.3.3: the remaining tiny positive diagonal perturbation in the reported corrected matrix sits only in the (1,1) entry.

theorem chapter03Example333_reportedCorrectedMatrix_decomposition : chapter03Example333ReportedCorrectedMatrix = chapter03Example333ReportedCorrectedMatrixCore + chapter03Example333ReportedTinyDiagonalCorrection

Helper for Chapter03 Example 3.3.3: the corrected matrix splits into the rational core plus the tiny nonnegative diagonal remainder.

theorem chapter03Example333_reportedCorrectedMatrixCore_isSymm : chapter03Example333ReportedCorrectedMatrixCore.IsSymm

Helper for Chapter03 Example 3.3.3: the rational core is symmetric.

theorem chapter03Example333_fin3_eq_zero_of_coords {x : Fin 3 → ℝ} (h0 : x 0 = 0) (h1 : x 1 = 0) (h2 : x 2 = 0) : x = 0

Helper for Chapter03 Example 3.3.3: if all three coordinates of a vector in Fin 3 → ℝ vanish, then the vector itself is zero.

theorem chapter03Example333_reportedCorrectedMatrixCore_quadraticForm_split (x : Fin 3 → ℝ) : x ⬝ᵥ chapter03Example333ReportedCorrectedMatrixCore.mulVec x = 3771 / 1000 * (x 0 + 1000 / 3771 * x 1 + 2000 / 3771 * x 2) ^ 2 + 2710792 / 471375 * (x 1 + 1164125 / 2710792 * x 2) ^ 2 + 47511304 / 42356125 * x 2 ^ 2

Helper for Chapter03 Example 3.3.3: the rational core quadratic form admits the exact two-step square-completion decomposition that mirrors the source's modified-factorization route.

theorem chapter03Example333_reportedCorrectedMatrixCore_dotProduct_pos {x : Fin 3 → ℝ} (hx : x ≠ 0) : 0 < x ⬝ᵥ chapter03Example333ReportedCorrectedMatrixCore.mulVec x

Helper for Chapter03 Example 3.3.3: the rational core already has a strictly positive quadratic form on every nonzero vector.

theorem chapter03Example333_reportedCorrectedMatrixCore_posDef : chapter03Example333ReportedCorrectedMatrixCore.PosDef

Helper for Chapter03 Example 3.3.3: the rational core matrix is positive definite.

theorem chapter03Example333_reportedTinyDiagonalCorrection_posSemidef : chapter03Example333ReportedTinyDiagonalCorrection.PosSemidef

Helper for Chapter03 Example 3.3.3: the tiny diagonal remainder is positive semidefinite, so it can be added without destroying positive definiteness.

theorem chapter03Example333_reportedCorrectedMatrix_posDef : chapter03Example333ReportedCorrectedMatrix.PosDef

Chapter03 Example 3.3.3 (5): the concrete corrected matrix Ḡ_k = G_k + E_k attached to the reported data is positive definite.

noncomputable def chapter03Example333ReportedRoundedFactorProduct : Matrix (Fin 3) (Fin 3) ℝ

The rounded factor product L D Lᵀ attached to the reported data of Example 3.3.3.