Andréief's identity over real or complex scalars

The RCLike formulation shares one proof between the real Zeta5 determinant and the complex Zeta32 contour determinant. The original real API is retained below. The real proof is from mo271/Zeta5 by Moritz Firsching; the scalar generalization is from Qian Tang's Zeta32 development, with its full attribution in LeanPool/Zeta32.lean.

noncomputable def Zeta5Irrational.AndreiefGeneral.permEquiv {n : ℕ} (τ : Equiv.Perm (Fin n)) : (Fin n → ℝ) ≃ᵐ (Fin n → ℝ)

The coordinate permutation x ↦ (i ↦ x (τ i)) as a measurable equivalence.

Equations

• Zeta5Irrational.AndreiefGeneral.permEquiv τ = MeasurableEquiv.arrowCongr' (Equiv.symm τ) (MeasurableEquiv.refl ℝ)

theorem Zeta5Irrational.AndreiefGeneral.permEquiv_apply {n : ℕ} (τ : Equiv.Perm (Fin n)) (x : Fin n → ℝ) (i : Fin n) : (permEquiv τ) x i = x (τ i)

theorem Zeta5Irrational.AndreiefGeneral.measurePreserving_permEquiv {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] (τ : Equiv.Perm (Fin n)) : MeasureTheory.MeasurePreserving (⇑(permEquiv τ)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)

noncomputable def Zeta5Irrational.AndreiefGeneral.andreiefI {n : ℕ} {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_1} [RCLike 𝕜] (f g : Fin n → ℝ → 𝕜) (ρ : Equiv.Perm (Fin n)) : 𝕜

The basic integral I(ρ) = ∫ ∏ᵢ f (ρ i) (xᵢ) g i (xᵢ).

Equations

• Zeta5Irrational.AndreiefGeneral.andreiefI f g ρ = ∫ (x : Fin n → ℝ), ∏ i : Fin n, f (ρ i) (x i) * g i (x i) ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ

theorem Zeta5Irrational.AndreiefGeneral.integral_prod_prod_eq {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] {𝕜 : Type u_1} [RCLike 𝕜] (f g : Fin n → ℝ → 𝕜) (σ τ : Equiv.Perm (Fin n)) : (∫ (x : Fin n → ℝ), (∏ i : Fin n, f (σ i) (x i)) * ∏ i : Fin n, g (τ i) (x i) ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ) = andreiefI f g (σ * τ⁻¹)

theorem Zeta5Irrational.AndreiefGeneral.andreief {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] {𝕜 : Type u_1} [RCLike 𝕜] (f g : Fin n → ℝ → 𝕜) (hfg : ∀ (i j : Fin n), MeasureTheory.Integrable (fun (x : ℝ) => f i x * g j x) μ) : (Matrix.of fun (i j : Fin n) => ∫ (x : ℝ), f i x * g j x ∂μ).det = 1 / ↑n.factorial * ∫ (x : Fin n → ℝ), (Matrix.of fun (i j : Fin n) => f i (x j)).det * (Matrix.of fun (i j : Fin n) => g i (x j)).det ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ

Andréief's identity.

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.permEquiv {n : ℕ} (τ : Equiv.Perm (Fin n)) : (Fin n → ℝ) ≃ᵐ (Fin n → ℝ)

Coordinate permutation, retained under the original real API.

Equations

• Zeta5Irrational.permEquiv τ = Zeta5Irrational.AndreiefGeneral.permEquiv τ

theorem Zeta5Irrational.permEquiv_apply {n : ℕ} (τ : Equiv.Perm (Fin n)) (x : Fin n → ℝ) (i : Fin n) : (permEquiv τ) x i = x (τ i)

theorem Zeta5Irrational.measurePreserving_permEquiv {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] (τ : Equiv.Perm (Fin n)) : MeasureTheory.MeasurePreserving (⇑(permEquiv τ)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.andreiefI {n : ℕ} {μ : MeasureTheory.Measure ℝ} (f g : Fin n → ℝ → ℝ) (ρ : Equiv.Perm (Fin n)) : ℝ

The real basic integral in Andréief's identity.

Equations

• Zeta5Irrational.andreiefI f g ρ = Zeta5Irrational.AndreiefGeneral.andreiefI f g ρ

theorem Zeta5Irrational.integral_prod_prod_eq {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] (f g : Fin n → ℝ → ℝ) (σ τ : Equiv.Perm (Fin n)) : (∫ (x : Fin n → ℝ), (∏ i : Fin n, f (σ i) (x i)) * ∏ i : Fin n, g (τ i) (x i) ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ) = andreiefI f g (σ * τ⁻¹)

theorem Zeta5Irrational.andreief {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.SigmaFinite μ] (f g : Fin n → ℝ → ℝ) (hfg : ∀ (i j : Fin n), MeasureTheory.Integrable (fun (x : ℝ) => f i x * g j x) μ) : (Matrix.of fun (i j : Fin n) => ∫ (x : ℝ), f i x * g j x ∂μ).det = 1 / ↑n.factorial * ∫ (x : Fin n → ℝ), (Matrix.of fun (i j : Fin n) => f i (x j)).det * (Matrix.of fun (i j : Fin n) => g i (x j)).det ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ

Andréief's identity, with the original real-valued statement.