noncomputable def PerronFrobeniusProof.QF {B : Type u_1} [Fintype B] (f : B → B → ℝ) (v : B → ℝ) : ℝ

The quadratic form $Q_f(v) = \sum_{s,t} v_s f_{st} v_t$ associated to a real symmetric matrix $f$.

noncomputable def PerronFrobeniusProof.BF {B : Type u_1} [Fintype B] (f : B → B → ℝ) (v w : B → ℝ) : ℝ

The bilinear form $B_f(v, w) = \sum_{s,t} v_s f_{st} w_t$ associated to a real symmetric matrix $f$.

theorem PerronFrobeniusProof.QF_eq_BF {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) : QF f v = BF f v v

The quadratic form is the diagonal of the bilinear form: $Q_f(v) = B_f(v, v)$.

theorem PerronFrobeniusProof.BF_add_left {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (u v w : B → ℝ) : BF f (fun (b : B) => u b + v b) w = BF f u w + BF f v w

Bilinearity (left): $B_f(u + v, w) = B_f(u, w) + B_f(v, w)$.

theorem PerronFrobeniusProof.BF_add_right {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (u v w : B → ℝ) : (BF f u fun (b : B) => v b + w b) = BF f u v + BF f u w

Bilinearity (right): $B_f(u, v + w) = B_f(u, v) + B_f(u, w)$.

theorem PerronFrobeniusProof.BF_smul_left {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (c : ℝ) (v w : B → ℝ) : BF f (fun (b : B) => c * v b) w = c * BF f v w

Scalar compatibility (left): $B_f(c \cdot v, w) = c \cdot B_f(v, w)$.

theorem PerronFrobeniusProof.BF_smul_right {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (c : ℝ) (v w : B → ℝ) : (BF f v fun (b : B) => c * w b) = c * BF f v w

Scalar compatibility (right): $B_f(v, c \cdot w) = c \cdot B_f(v, w)$.

theorem PerronFrobeniusProof.QF_add_smul {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v w : B → ℝ) (c : ℝ) : (QF f fun (b : B) => v b + c * w b) = QF f v + c * (BF f v w + BF f w v) + c ^ 2 * QF f w

Polarization identity: $Q_f(v + cw) = Q_f(v) + c(B_f(v,w) + B_f(w,v)) + c^2 Q_f(w)$.

theorem PerronFrobeniusProof.BF_left_single {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (i : B) : BF f (Pi.single i 1) v = ∑ t : B, f i t * v t

Evaluation at a basis vector on the left: $B_f(e_i, v) = \sum_t f_{i,t} v_t = (f v)_i$.

theorem PerronFrobeniusProof.BF_right_single {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (i : B) : BF f v (Pi.single i 1) = ∑ s : B, v s * f s i

Evaluation at a basis vector on the right: $B_f(v, e_i) = \sum_s v_s f_{s,i} = (v f)_i$.

theorem PerronFrobeniusProof.BF_sum_eq_zero {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (hPSD : ∀ (u : B → ℝ), QF f u ≥ 0) (hQv : QF f v = 0) (w : B → ℝ) : BF f v w + BF f w v = 0

Kernel orthogonality: if $Q_f(v) = 0$ and the form is PSD, then $B_f(v, w) + B_f(w, v) = 0$ for all $w$. (This is essentially that $v$ is in the radical of the symmetrized form.)

theorem PerronFrobeniusProof.combined_row_sum {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (i : B) (hBF_zero : ∀ (w : B → ℝ), BF f v w + BF f w v = 0) : ∑ t : B, (f i t + f t i) * v t = 0

Row equation: orthogonality of $v$ to $e_i$ gives $\sum_t (f_{it} + f_{ti}) v_t = 0$ for each row $i$.

theorem PerronFrobeniusProof.abs_sq_mul (a c : ℝ) : |a| * c * |a| = a * c * a

$|a| \cdot c \cdot |a| = a \cdot c \cdot a$ since $|a|^2 = a^2$.

theorem PerronFrobeniusProof.abs_mul_neg_le (a b c : ℝ) (hc : c ≤ 0) : |a| * c * |b| ≤ a * c * b

Sign-flip inequality: for $c \le 0$, $|a| \cdot c \cdot |b| \le a \cdot c \cdot b$ (note the direction reversal from the Cauchy–Schwarz inequality $a b \le |a| |b|$ scaled by a negative).

theorem PerronFrobeniusProof.QF_abs_le {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) : (QF f fun (b : B) => |v b|) ≤ QF f v

Absolute-value monotonicity: for a matrix with $f_{st} \le 0$ off-diagonal, $Q_f(|v|) \le Q_f(v)$ (i.e. taking absolute values only decreases the quadratic form).

theorem PerronFrobeniusProof.sum_eq_zero_of_nonpos' {ι : Type u_2} {s : Finset ι} {g : ι → ℝ} (h_nonpos : ∀ i ∈ s, g i ≤ 0) (h_sum : ∑ i ∈ s, g i = 0) (i : ι) : i ∈ s → g i = 0

A sum of nonpositive reals which equals zero must be termwise zero.

theorem PerronFrobeniusProof.offdiag_zero_from_row {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) (i j : B) (hij : i ≠ j) (hv_nonneg : ∀ (b : B), v b ≥ 0) (hvi : v i = 0) (hvj : v j > 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) (hrow : ∑ t : B, (f i t + f t i) * v t = 0) : f i j = 0 ∧ f j i = 0

Zero-block lemma: if the row equation $\sum_t (f_{it} + f_{ti}) v_t = 0$ holds with $v \ge 0$, $v_i = 0$, $v_j > 0$, and $f_{st} \le 0$ off-diagonal, then $f_{ij} = f_{ji} = 0$.

theorem PerronFrobeniusProof.nonneg_kernel_pos {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v : B → ℝ) [Nonempty B] (hPSD : ∀ (u : B → ℝ), QF f u ≥ 0) (hQv : QF f v = 0) (hv_nonneg : ∀ (b : B), v b ≥ 0) (hv_ne : v ≠ 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) (hIndecomp : CoxeterGroup.FormIndecomposable f) (b : B) : v b > 0

Perron–Frobenius positivity: a nonnegative null vector $v \ge 0$, $Q_f(v) = 0$, $v \ne 0$ in the kernel of an indecomposable PSD off-diagonal-nonpositive form $f$ must be strictly positive component-wise.

theorem PerronFrobeniusProof.positive_kernel_proportional {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v w : B → ℝ) [Nonempty B] (hPSD : ∀ (u : B → ℝ), QF f u ≥ 0) (hQv : QF f v = 0) (hQw : QF f w = 0) (hv_pos : ∀ (b : B), v b > 0) (_hw_pos : ∀ (b : B), w b > 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) (hIndecomp : CoxeterGroup.FormIndecomposable f) : ∃ (c : ℝ), w = fun (b : B) => c * v b

One-dimensional kernel (positive case): any two strictly positive null vectors $v, w > 0$ of an indecomposable PSD off-diagonal-nonpositive form are scalar multiples: $w = c \cdot v$.

theorem PerronFrobeniusProof.kernel_scalar_multiple {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) (v w : B → ℝ) [Nonempty B] (hPSD : ∀ (u : B → ℝ), QF f u ≥ 0) (hv_pos : ∀ (b : B), v b > 0) (hQv : QF f v = 0) (hQw : QF f w = 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) (hIndecomp : CoxeterGroup.FormIndecomposable f) : ∃ (c : ℝ), w = fun (b : B) => c * v b

One-dimensional kernel (general case): given a strictly positive null vector $v > 0$, any other null vector $w$ is a scalar multiple of $v$: $w = c \cdot v$.

instance PerronFrobeniusProof.perronFrobeniusInstance {B : Type u_1} [DecidableEq B] [Fintype B] (f : B → B → ℝ) [Nonempty B] : PerronFrobeniusProperty f

Perron–Frobenius instance: every off-diagonal-nonpositive real matrix on a nonempty index type automatically satisfies the PerronFrobeniusProperty.