Theory Andreief_Identity
theory Andreief_Identity
imports "Jordan_Normal_Form.Determinant" "HOL-Analysis.Analysis"
begin
section ‹Andreief's identity (continuous Cauchy--Binet)›
text ‹For a ‹σ›-finite measure ‹μ› and functions
‹φ⇩i, ψ⇩j› with ‹φ⇩i ψ⇩j›
integrable,
‹det [∫ φ⇩i ψ⇩j dμ] =
(1/n!) ∫ det [φ⇩a(x⇩b)] det [ψ⇩a(x⇩b)]
dμ⇧⊗⇧n›, with the determinants of the
Jordan\_Normal\_Form library and the product measure @{const PiM}; also the transposition and
column-scaling rules for determinants used with it.›
text ‹The general continuous Cauchy-Binet (Andreief) identity:
@{text "det[∫ φ_i ψ_j dmu] =
(1/n!) ∫ det[φ_a(x_b)] det[ψ_a(x_b)] dmu^{⊗n}"}. Proof: Leibniz
expansion,
symmetrisation over permutations, Fubini on @{text "PiM"}.›
theorem andreief:
fixes μ :: "real measure" and φ ψ :: "nat ⇒ real ⇒ real" and
n :: nat
assumes sf: "sigma_finite_measure μ"
and integ: "⋀i j. i < n ⟹ j < n ⟹
integrable μ (λx. φ i x * ψ j x)"
shows "Determinant.det (Matrix.mat n n (λ(i,
j). integral⇧L μ (λx. φ i x * ψ j x))) =
1 / fact n * integral⇧L (PiM {..<n} (λ_. μ))
(λx. Determinant.det (Matrix.mat n n (λ(a, b). φ a (x b))) *
Determinant.det (Matrix.mat n n (λ(a, b). ψ a (x b))))"
proof -
define G :: "nat ⇒ nat ⇒ real" where "G =
(λi j. integral⇧L μ (λx. φ i x * ψ j x))"
define P :: "(nat ⇒ nat) set" where "P = {p. p permutes {0..<n}}"
interpret product_sigma_finite "λ_::nat. μ"
by (rule product_sigma_finite.intro) (rule sf)
have cardP: "card P = fact n"
unfolding P_def by (simp add: card_permutations)
have inP: "⋀σ a. σ ∈ P ⟹ a < n ⟹
σ a < n"
by (simp add: P_def permutes_in_image)
have permP: "⋀σ. σ ∈ P ⟹ σ permutes {..<n}"
by (simp add: P_def atLeast0LessThan)
have permutationP: "⋀σ. σ ∈ P ⟹ permutation σ"
by (auto simp: P_def permutes_imp_permutation intro: permutes_imp_permutation)
text ‹Leibniz formula in column form:
@{text "det (f a b)_{a,b} = ∑_σ sgn σ ∏_a f (σ a) a"}.›
have colform: "Determinant.det (Matrix.mat n n (λ(a, b). f a b)) = (∑ σ ∈
P. signof σ * (∏ a < n. f (σ a) a))"
for f :: "nat ⇒ nat ⇒ real"
proof -
have "Determinant.det (Matrix.mat n n (λ(a, b). f a b)) =
Determinant.det (transpose_mat (Matrix.mat n n (λ(a, b). f a b)))"
by (simp add: Determinant.det_transpose[OF mat_carrier])
also have "… = (∑ σ ∈ P. signof σ * (∏ a =
0..<n. transpose_mat (Matrix.mat n n (λ(a, b). f a b)) $$ (a, σ a)))"
by (simp add: det_def'[of _ n] P_def)
also have "… = (∑ σ ∈ P. signof σ * (∏ a <
n. f (σ a) a))"
by (simp add: inP atLeast0LessThan)
finally show ?thesis .
qed
have detA: "⋀x. Determinant.det (Matrix.mat n n (λ(a, b). φ a (x b))) =
(∑ σ ∈ P. signof σ * (∏ a < n. φ (σ a) (x a)))"
by (simp add: colform)
have detB: "⋀x. Determinant.det (Matrix.mat n n (λ(a, b). ψ a (x b))) =
(∑ τ ∈ P. signof τ * (∏ a < n. ψ (τ a) (x a)))"
by (simp add: colform)
have leib: "⋀x. Determinant.det (Matrix.mat n n (λ(a,
b). φ a (x b))) * Determinant.det (Matrix.mat n n (λ(a, b). ψ a (x b)))
= (∑ σ ∈ P. ∑ τ ∈
P. signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)))"
unfolding detA detB sum_product prod.distrib by (simp add: mult_ac)
text ‹Integrate each term with Fubini on the finite product.›
have integ_a: "⋀σ τ a. σ ∈ P ⟹
τ ∈ P ⟹ a < n ⟹
integrable μ (λx. φ (σ a) x * ψ (τ a) x)"
using integ inP by simp
have intg: "⋀σ τ. σ ∈ P ⟹
τ ∈ P ⟹ integrable (PiM {..<n} (λ_. μ)) (λx.
∏ a < n. φ (σ a) (x a) * ψ (τ a) (x a))"
proof -
fix σ τ assume s: "σ ∈ P" and t: "τ ∈ P"
show "integrable (PiM {..<n} (λ_. μ)) (λx. ∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a))"
using product_integrable_prod[of "{..<n}" "λa x. φ (σ a) x *
ψ (τ a) x"] integ_a[OF s t] by simp
qed
have int: "⋀σ τ. σ ∈ P ⟹
τ ∈ P ⟹
integral⇧L (PiM {..<n} (λ_. μ)) (λx. ∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)) = (∏ a <
n. G (σ a) (τ a))"
proof -
fix σ τ assume s: "σ ∈ P" and t: "τ ∈ P"
show "integral⇧L (PiM {..<n} (λ_. μ)) (λx. ∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)) = (∏ a <
n. G (σ a) (τ a))"
using product_integral_prod[of "{..<n}" "λa x. φ (σ a) x *
ψ (τ a) x"] integ_a[OF s t] by (simp add: G_def)
qed
have E: "integral⇧L (PiM {..<n} (λ_. μ)) (λx. Determinant.det
(Matrix.mat n n (λ(a, b). φ a (x b))) *
Determinant.det (Matrix.mat n n (λ(a, b). ψ a (x b))))
= (∑ σ ∈ P. ∑ τ ∈
P. signof σ * signof τ * (∏ a < n. G (σ a) (τ a)))"
proof -
have i1: "⋀σ τ. σ ∈ P ⟹
τ ∈ P ⟹ integrable (PiM {..<n} (λ_. μ)) (λx.
signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)))"
using intg by simp
have i2: "⋀σ. σ ∈ P ⟹
integrable (PiM {..<n} (λ_. μ)) (λx. ∑ τ ∈
P. signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)))"
using i1 by (auto intro: Bochner_Integration.integrable_sum)
have "integral⇧L (PiM {..<n} (λ_. μ)) (λx. Determinant.det (Matrix.mat
n n (λ(a, b). φ a (x b))) * Determinant.det (Matrix.mat n n (λ(a,
b). ψ a (x b))))
= integral⇧L (PiM {..<n} (λ_. μ)) (λx. ∑ σ ∈
P. ∑ τ ∈ P. signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)))"
by (simp add: leib)
also have "… = (∑ σ ∈ P. ∑ τ ∈
P. integral⇧L (PiM {..<n} (λ_. μ)) (λx. signof σ *
signof τ * (∏ a < n. φ (σ a) (x a) * ψ (τ a) (x a))))"
proof -
have "integral⇧L (PiM {..<n} (λ_. μ)) (λx. ∑ σ ∈
P. ∑ τ ∈ P. signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a)))
= (∑ σ ∈ P. integral⇧L (PiM {..<n} (λ_. μ)) (λx.
∑ τ ∈ P. signof σ * signof τ * (∏ a <
n. φ (σ a) (x a) * ψ (τ a) (x a))))"
using i2 by (auto intro: Bochner_Integration.integral_sum)
also have "… = (∑ σ ∈ P. ∑ τ ∈
P. integral⇧L (PiM {..<n} (λ_. μ)) (λx. signof σ *
signof τ * (∏ a < n. φ (σ a) (x a) * ψ (τ a) (x a))))"
using i1 by (simp add: Bochner_Integration.integral_sum)
finally show ?thesis .
qed
also have "… = (∑ σ ∈ P. ∑ τ ∈
P. signof σ * signof τ * (∏ a < n. G (σ a) (τ a)))"
proof (rule sum.cong[OF refl], rule sum.cong[OF refl])
fix σ τ assume s: "σ ∈ P" and t: "τ ∈ P"
show "integral⇧L (PiM {..<n} (λ_. μ)) (λx. signof σ *
signof τ * (∏ a < n. φ (σ a) (x a) * ψ (τ a) (x a))) =
signof σ * signof τ * (∏ a < n. G (σ a) (τ a))"
using int[OF s t] by simp
qed
finally show ?thesis .
qed
text ‹For fixed @{text τ}, substitute
@{text "ρ = σ ∘ Hilbert_Choice.inv τ"}: the inner sum is
@{text "det G"}.›
have reidx: "⋀σ τ. σ ∈ P ⟹
τ ∈ P ⟹ (∏ a < n. G (σ a) (τ a)) = (∏ b <
n. G ((σ ∘ Hilbert_Choice.inv τ) b) b)"
proof -
fix σ τ assume s: "σ ∈ P" and t: "τ ∈ P"
show "(∏ a < n. G (σ a) (τ a)) = (∏ b <
n. G ((σ ∘ Hilbert_Choice.inv τ) b) b)"
using prod.permute[OF permP[OF t],
of "λb. G ((σ ∘ Hilbert_Choice.inv τ) b) b"] permutes_inverses[OF
permP[OF t]] by (simp add: o_def)
qed
have signmul: "⋀σ τ. σ ∈ P ⟹
τ ∈ P ⟹ (signof σ :: real) * signof τ =
signof (σ ∘ Hilbert_Choice.inv τ)"
proof -
fix σ τ assume s: "σ ∈ P" and t: "τ ∈ P"
show "(signof σ :: real) * signof τ =
signof (σ ∘ Hilbert_Choice.inv τ)"
using sign_compose[OF permutationP[OF s] permutation_inverse[OF permutationP[OF t]]]
sign_inverse[OF permutationP[OF t]] by simp
qed
have bij: "⋀τ. τ ∈ P ⟹
bij_betw (λσ. σ ∘ Hilbert_Choice.inv τ) P P"
proof -
fix τ assume t: "τ ∈ P"
have tp: "τ permutes {0..<n}" using t by (simp add: P_def)
have h1: "(λσ. σ ∘ Hilbert_Choice.inv τ) ∈
P → P"
using permutes_compose[OF permutes_inv[OF tp]] by (simp add: P_def)
have h2: "(λρ. ρ ∘ τ) ∈ P → P"
using permutes_compose[OF tp] by (simp add: P_def)
have h3: "⋀σ. σ ∈ P ⟹
σ ∘ Hilbert_Choice.inv τ ∘ τ = σ"
by (simp add: o_assoc[symmetric] permutes_inv_o[OF tp])
have h4: "⋀ρ. ρ ∈ P ⟹
ρ ∘ τ ∘ Hilbert_Choice.inv τ = ρ"
by (simp add: o_assoc[symmetric] permutes_inv_o[OF tp])
show "bij_betw (λσ. σ ∘ Hilbert_Choice.inv τ) P P"
using bij_betwI[OF h1 h2] h3 h4 by simp
qed
have inner: "⋀τ. τ ∈ P ⟹
(∑ σ ∈ P. signof σ * signof τ * (∏ a <
n. G (σ a) (τ a))) = Determinant.det (Matrix.mat n n (λ(i, j). G i j))"
proof -
fix τ assume t: "τ ∈ P"
have "(∑ σ ∈ P. signof σ * signof τ * (∏ a <
n. G (σ a) (τ a))) = (∑ σ ∈
P. signof (σ ∘ Hilbert_Choice.inv τ) * (∏ b <
n. G ((σ ∘ Hilbert_Choice.inv τ) b) b))"
by (simp add: reidx[OF _ t] signmul[OF _ t])
also have "… = (∑ ρ ∈ P. signof ρ * (∏ b < n. G (ρ b) b))"
using sum.reindex_bij_betw[OF bij[OF t], of "λρ. signof ρ * (∏ b <
n. G (ρ b) b)"] by simp
also have "… = Determinant.det (Matrix.mat n n (λ(i, j). G i j))"
using colform[of G] by simp
finally show "(∑ σ ∈ P. signof σ * signof τ * (∏ a <
n. G (σ a) (τ a))) = Determinant.det (Matrix.mat n n (λ(i, j). G i j))" .
qed
have comb: "(∑ σ ∈ P. ∑ τ ∈
P. signof σ * signof τ * (∏ a < n. G (σ a) (τ a))) =
fact n * Determinant.det (Matrix.mat n n (λ(i, j). G i j))"
proof -
have "(∑ σ ∈ P. ∑ τ ∈
P. signof σ * signof τ * (∏ a < n. G (σ a) (τ a))) =
(∑ τ ∈ P. ∑ σ ∈
P. signof σ * signof τ * (∏ a < n. G (σ a) (τ a)))"
using sum.swap by fast
also have "… = (∑ τ ∈
P. Determinant.det (Matrix.mat n n (λ(i, j). G i j)))"
by (simp add: inner)
also have "… = fact n * Determinant.det (Matrix.mat n n (λ(i, j). G i j))"
by (simp add: cardP)
finally show ?thesis .
qed
have fn: "(fact n :: real) ≠ 0" by simp
show ?thesis
unfolding G_def [symmetric] E comb using fn by simp
qed
text ‹(6.10): @{text "Δ_K(ζ(5)) =
(1/h!) ∫_{(0,∞)^h} ∏_{i<j}(y_i^2 -
y_j^2)^2 ∏_i D_N(y_i^2)^6/D_K(y_i^2) w(y_i) dy"}.›
lemma andreief_det_swap:
fixes f :: "nat ⇒ nat ⇒ 'a :: comm_ring_1"
shows "Determinant.det (Matrix.mat n n (λ(a, b). f b a)) =
Determinant.det (Matrix.mat n n (λ(a, b). f a b))"
proof -
have "Matrix.mat n n (λ(a, b). f b a) =
transpose_mat (Matrix.mat n n (λ(a, b). f a b))"
by (auto intro: eq_matI)
thus ?thesis
using Determinant.det_transpose[OF mat_carrier] by auto
qed
lemma andreief_det_scale_cols:
fixes f :: "nat ⇒ nat ⇒ 'a :: comm_ring_1" and c :: "nat ⇒ 'a"
shows "Determinant.det (Matrix.mat n n (λ(a, b). f a b * c b)) = (∏ b <
n. c b) * Determinant.det (Matrix.mat n n (λ(a, b). f a b))"
proof -
have inP: "⋀p j. p permutes {0..<n} ⟹ j < n ⟹ p j < n"
by (simp add: permutes_in_image)
have d1: "Determinant.det (Matrix.mat n n (λ(a, b). f a b * c b)) =
(∑ p | p permutes {0..<n}. signof p * (∏ j < n. f (p j) j * c j))"
by (simp add: det_col[OF mat_carrier] inP)
have d2: "Determinant.det (Matrix.mat n n (λ(a, b). f a b)) =
(∑ p | p permutes {0..<n}. signof p * (∏ j < n. f (p j) j))"
by (simp add: det_col[OF mat_carrier] inP)
show ?thesis
unfolding d1 d2 prod.distrib sum_distrib_left
by (simp add: mult_ac)
qed
end