TwoD: refactor SemiDegenerate + PureQuartic through AddSeparable (Tide 13)

Laplace/TwoD/AddSeparable.lean

@@ -55,12 +55,12 @@ lemma exp_neg_t_addSeparable_eq_mul (U V : ℝ → ℝ) (t : ℝ) (z : ℝ × 
       show (-(t * (U z.1 + V z.2)) : ℝ) = -(t * U z.1) + -(t * V z.2) from by ring,
       Real.exp_add]
 
-/-- **Partition-function factorisation**: under integrability of each marginal
-Boltzmann weight, `Z_2D(t) = Z_U(t) · Z_V(t)`. -/
+/-- **Partition-function factorisation**: `Z_2D(t) = Z_U(t) · Z_V(t)`.
+Unconditional: `MeasureTheory.integral_prod_mul` is unconditional, so the
+factorisation holds even when the 1D weights are not Lebesgue-integrable
+(both sides are `0` by Bochner convention in that case). -/
 theorem partitionFunction_addSeparable_factor
-    {U V : ℝ → ℝ} {t : ℝ}
-    (_hU : Integrable (fun x : ℝ => Real.exp (-(t * U x))))
-    (_hV : Integrable (fun y : ℝ => Real.exp (-(t * V y)))) :
+    (U V : ℝ → ℝ) (t : ℝ) :
     partitionFunction (addSeparable U V) t =
       Laplace.partitionFunction U t * Laplace.partitionFunction V t := by
   unfold partitionFunction Laplace.partitionFunction
@@ -73,11 +73,10 @@ theorem partitionFunction_addSeparable_factor
     (g := fun y : ℝ => Real.exp (-(t * V y)))
 
 /-- **Separable-observable factorisation**: for an integrand `f(x) · g(y) · e^{-tL}`,
-the 2D integral factors as a product of 1D weighted integrals. -/
+the 2D integral factors as a product of 1D weighted integrals.
+Unconditional, for the same reason as `partitionFunction_addSeparable_factor`. -/
 theorem integral_separable_addSeparable
-    {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ)
-    (_hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x))))
-    (_hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) :
+    (U V : ℝ → ℝ) (t : ℝ) (f g : ℝ → ℝ) :
     (∫ z : ℝ × ℝ, f z.1 * g z.2 * Real.exp (-(t * addSeparable U V z))) =
       (∫ x : ℝ, f x * Real.exp (-(t * U x))) *
         (∫ y : ℝ, g y * Real.exp (-(t * V y))) := by
@@ -97,17 +96,13 @@ nonzero, the 2D Gibbs expectation of a separable observable factors. -/
 theorem gibbsExpectation_separable_addSeparable
     {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ)
     (hZU_ne : Laplace.partitionFunction U t ≠ 0)
-    (hZV_ne : Laplace.partitionFunction V t ≠ 0)
-    (hU : Integrable (fun x : ℝ => Real.exp (-(t * U x))))
-    (hV : Integrable (fun y : ℝ => Real.exp (-(t * V y))))
-    (hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x))))
-    (hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) :
+    (hZV_ne : Laplace.partitionFunction V t ≠ 0) :
     gibbsExpectation (addSeparable U V) t (fun z => f z.1 * g z.2) =
       Laplace.gibbsExpectation U t f *
         Laplace.gibbsExpectation V t g := by
   unfold gibbsExpectation Laplace.gibbsExpectation
-  rw [partitionFunction_addSeparable_factor hU hV]
-  rw [integral_separable_addSeparable f g hf hg]
+  rw [partitionFunction_addSeparable_factor]
+  rw [integral_separable_addSeparable]
   field_simp
 
 /-- **Mixed-covariance vanishing**: under a product/separable Gibbs measure,
@@ -116,24 +111,17 @@ observable is zero. The structural payoff of separability. -/
 theorem gibbsCov_addSeparable_fst_snd_eq_zero
     {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ)
     (hZU_ne : Laplace.partitionFunction U t ≠ 0)
-    (hZV_ne : Laplace.partitionFunction V t ≠ 0)
-    (hU : Integrable (fun x : ℝ => Real.exp (-(t * U x))))
-    (hV : Integrable (fun y : ℝ => Real.exp (-(t * V y))))
-    (hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x))))
-    (hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) :
+    (hZV_ne : Laplace.partitionFunction V t ≠ 0) :
     gibbsCov (addSeparable U V) t
         (fun z => f z.1) (fun z => g z.2) = 0 := by
   unfold gibbsCov
   -- Step 1: ⟨f(z.1) · g(z.2)⟩ = ⟨f⟩_U · ⟨g⟩_V (separable-observable factorisation).
-  rw [show (fun z : ℝ × ℝ => f z.1 * g z.2) =
-        (fun z : ℝ × ℝ => f z.1 * g z.2) from rfl]
-  rw [gibbsExpectation_separable_addSeparable f g hZU_ne hZV_ne hU hV hf hg]
+  rw [gibbsExpectation_separable_addSeparable f g hZU_ne hZV_ne]
   -- Step 2: ⟨f(z.1)⟩_2D = ⟨f⟩_U (collapse with g = 1).
   have hExp_f : gibbsExpectation (addSeparable U V) t (fun z => f z.1) =
       Laplace.gibbsExpectation U t f := by
     have h := gibbsExpectation_separable_addSeparable f (fun _ => (1 : ℝ))
-      hZU_ne hZV_ne hU hV hf
-      (by simpa using hV)
+      hZU_ne hZV_ne
     have hg1 : Laplace.gibbsExpectation V t (fun _ => (1 : ℝ)) = 1 :=
       Laplace.gibbsExpectation_const V t 1 hZV_ne
     rw [show (fun z : ℝ × ℝ => f z.1 * (1 : ℝ)) = (fun z : ℝ × ℝ => f z.1) from by
@@ -143,8 +131,7 @@ theorem gibbsCov_addSeparable_fst_snd_eq_zero
   have hExp_g : gibbsExpectation (addSeparable U V) t (fun z => g z.2) =
       Laplace.gibbsExpectation V t g := by
     have h := gibbsExpectation_separable_addSeparable (fun _ => (1 : ℝ)) g
-      hZU_ne hZV_ne hU hV
-      (by simpa using hU) hg
+      hZU_ne hZV_ne
     have hf1 : Laplace.gibbsExpectation U t (fun _ => (1 : ℝ)) = 1 :=
       Laplace.gibbsExpectation_const U t 1 hZU_ne
     rw [show (fun z : ℝ × ℝ => (1 : ℝ) * g z.2) = (fun z : ℝ × ℝ => g z.2) from by

Laplace/TwoD/PureQuartic.lean

@@ -65,35 +65,38 @@ noncomputable def pureQuarticPotential : ℝ × ℝ → ℝ :=
 
 /-! ## Boltzmann factor decomposition -/
 
+/-! ## Bridge to the additively-separable abstraction -/
+
+/-- The pure-quartic 2D potential is an additively-separable potential
+with both marginals equal to the 1D quartic. -/
+@[simp] lemma pureQuarticPotential_eq_addSeparable :
+    pureQuarticPotential =
+      addSeparable Laplace.OneD.quarticPotential Laplace.OneD.quarticPotential := by
+  funext z
+  simp only [pureQuarticPotential_apply, addSeparable_apply,
+    Laplace.OneD.quarticPotential_apply]
+
 /-- The Boltzmann factor for `L(x,y) = x⁴/24 + y⁴/24` factorises as a product
-of quartic factors in `x` and `y`. -/
+of quartic factors in `x` and `y`. Corollary of `exp_neg_t_addSeparable_eq_mul`
+via the bridge above. -/
 lemma exp_neg_t_pureQuartic_eq_mul (t : ℝ) (z : ℝ × ℝ) :
     Real.exp (-(t * pureQuarticPotential z)) =
       Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) *
       Real.exp (-(t * Laplace.OneD.quarticPotential z.2)) := by
-  rw [pureQuarticPotential_apply, Laplace.OneD.quarticPotential_apply,
-      Laplace.OneD.quarticPotential_apply]
-  rw [show -(t * (z.1 ^ 4 / 24 + z.2 ^ 4 / 24)) =
-        -(t * (z.1 ^ 4 / 24)) + -(t * (z.2 ^ 4 / 24)) from by ring]
-  exact Real.exp_add _ _
+  rw [pureQuarticPotential_eq_addSeparable]
+  exact exp_neg_t_addSeparable_eq_mul _ _ t z
 
 /-! ## Partition function factorisation -/
 
 /-- The 2D partition function factorises into the square of the 1D quartic
-partition function. -/
+partition function. Application of `partitionFunction_addSeparable_factor`
+via the bridge. -/
 theorem partitionFunction_factor (t : ℝ) :
     partitionFunction pureQuarticPotential t =
       Laplace.partitionFunction Laplace.OneD.quarticPotential t *
       Laplace.partitionFunction Laplace.OneD.quarticPotential t := by
-  unfold partitionFunction Laplace.partitionFunction
-  rw [show (fun z : ℝ × ℝ => Real.exp (-(t * pureQuarticPotential z))) =
-        (fun z : ℝ × ℝ =>
-          Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) *
-          Real.exp (-(t * Laplace.OneD.quarticPotential z.2))) from by
-        funext z; exact exp_neg_t_pureQuartic_eq_mul t z]
-  exact MeasureTheory.integral_prod_mul
-    (f := fun x : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential x)))
-    (g := fun y : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential y)))
+  rw [pureQuarticPotential_eq_addSeparable]
+  exact partitionFunction_addSeparable_factor _ _ _
 
 /-- Closed form for the partition function:
 `Z_2D(t) = ((1/2) · (24/t)^{1/4} · Γ(1/4))²`. -/
@@ -114,23 +117,15 @@ theorem partitionFunction_pos {t : ℝ} (ht : 0 < t) :
 
 /-- The 2D moment integral of a separable monomial `z.1^m · z.2^n` against
 the pure-quartic Gibbs weight factorises into the product of 1D moment
-integrals. -/
+integrals. Application of `integral_separable_addSeparable` at
+`f = fun x ↦ x^m`, `g = fun y ↦ y^n` via the bridge. -/
 theorem integral_pow_pow_factor (t : ℝ) (m n : ℕ) :
     (∫ z : ℝ × ℝ, z.1 ^ m * z.2 ^ n *
         Real.exp (-(t * pureQuarticPotential z))) =
       (∫ x : ℝ, x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) *
       (∫ y : ℝ, y ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential y))) := by
-  rw [show (fun z : ℝ × ℝ => z.1 ^ m * z.2 ^ n *
-            Real.exp (-(t * pureQuarticPotential z))) =
-        (fun z : ℝ × ℝ =>
-          (z.1 ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential z.1))) *
-          (z.2 ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential z.2)))) from by
-        funext z
-        rw [exp_neg_t_pureQuartic_eq_mul t z]
-        ring]
-  exact MeasureTheory.integral_prod_mul
-    (f := fun x : ℝ => x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x)))
-    (g := fun y : ℝ => y ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential y)))
+  simp only [pureQuarticPotential_eq_addSeparable]
+  exact integral_separable_addSeparable _ _ _ (fun x => x ^ m) (fun y => y ^ n)
 
 /-! ## Specialised moments needed for affine covariance -/
 

Laplace/TwoD/SemiDegenerate.lean

@@ -73,39 +73,43 @@ noncomputable def semiDegeneratePotential (lam : ℝ) : ℝ × ℝ → ℝ :=
 @[simp] lemma semiDegeneratePotential_apply (lam : ℝ) (z : ℝ × ℝ) :
     semiDegeneratePotential lam z = lam / 2 * z.2 ^ 2 + z.1 ^ 4 / 24 := rfl
 
+/-! ## Bridge to the additively-separable abstraction -/
+
+/-- The semi-degenerate potential is an additively-separable potential
+with `U = quartic` and `V = harmonic`. -/
+@[simp] lemma semiDegeneratePotential_eq_addSeparable (lam : ℝ) :
+    semiDegeneratePotential lam =
+      addSeparable Laplace.OneD.quarticPotential
+        (Laplace.OneD.harmonicPotential lam) := by
+  funext z
+  simp only [semiDegeneratePotential_apply, addSeparable_apply,
+    Laplace.OneD.quarticPotential_apply]
+  unfold Laplace.OneD.harmonicPotential
+  ring
+
 /-! ## Boltzmann factor decomposition -/
 
 /-- The Boltzmann factor for `L(x,y) = (λ/2)y² + x⁴/24` factorises as a
-product of a quartic factor in `x` and a harmonic factor in `y`. -/
+product of a quartic factor in `x` and a harmonic factor in `y`. Corollary
+of `exp_neg_t_addSeparable_eq_mul` via the bridge above. -/
 lemma exp_neg_t_semiDegenerate_eq_mul (lam t : ℝ) (z : ℝ × ℝ) :
     Real.exp (-(t * semiDegeneratePotential lam z)) =
       Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) *
       Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2)) := by
-  rw [semiDegeneratePotential_apply, Laplace.OneD.quarticPotential_apply]
-  unfold Laplace.OneD.harmonicPotential
-  rw [show -(t * (lam / 2 * z.2 ^ 2 + z.1 ^ 4 / 24)) =
-        -(t * (z.1 ^ 4 / 24)) + -(t * (lam / 2 * z.2 ^ 2)) from by ring]
-  exact Real.exp_add _ _
+  rw [semiDegeneratePotential_eq_addSeparable]
+  exact exp_neg_t_addSeparable_eq_mul _ _ t z
 
 /-! ## Partition function factorisation -/
 
 /-- The 2D partition function factorises into the product of the 1D
-quartic and 1D harmonic partition functions. -/
+quartic and 1D harmonic partition functions. Application of
+`partitionFunction_addSeparable_factor` via the bridge. -/
 theorem partitionFunction_factor (lam t : ℝ) :
     partitionFunction (semiDegeneratePotential lam) t =
       Laplace.partitionFunction Laplace.OneD.quarticPotential t *
       Laplace.partitionFunction (Laplace.OneD.harmonicPotential lam) t := by
-  unfold partitionFunction Laplace.partitionFunction
-  -- Decompose the Boltzmann factor pointwise.
-  rw [show (fun z : ℝ × ℝ => Real.exp (-(t * semiDegeneratePotential lam z))) =
-        (fun z : ℝ × ℝ =>
-          Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) *
-          Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2))) from by
-        funext z; exact exp_neg_t_semiDegenerate_eq_mul lam t z]
-  -- Apply Fubini-style factorisation for product integrals of separable functions.
-  exact MeasureTheory.integral_prod_mul
-    (f := fun x : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential x)))
-    (g := fun y : ℝ => Real.exp (-(t * Laplace.OneD.harmonicPotential lam y)))
+  rw [semiDegeneratePotential_eq_addSeparable]
+  exact partitionFunction_addSeparable_factor _ _ _
 
 /-- Closed form for the partition function: `Z_2D(t) = (1/2)·(24/t)^{1/4}·Γ(1/4)·√(2π/(λt))`. -/
 theorem partitionFunction_closed_form {lam t : ℝ} (hlam : 0 < lam) (ht : 0 < t) :
@@ -126,23 +130,15 @@ theorem partitionFunction_pos {lam t : ℝ} (hlam : 0 < lam) (ht : 0 < t) :
 
 /-- The 2D moment integral of a separable monomial `z.1^m · z.2^n` against
 the semi-degenerate Gibbs weight factorises into the product of 1D
-moment integrals. -/
+moment integrals. Application of `integral_separable_addSeparable` at
+`f = fun x ↦ x^m`, `g = fun y ↦ y^n` via the bridge. -/
 theorem integral_pow_pow_factor (lam t : ℝ) (m n : ℕ) :
     (∫ z : ℝ × ℝ, z.1 ^ m * z.2 ^ n *
         Real.exp (-(t * semiDegeneratePotential lam z))) =
       (∫ x : ℝ, x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) *
       (∫ y : ℝ, y ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam y))) := by
-  rw [show (fun z : ℝ × ℝ => z.1 ^ m * z.2 ^ n *
-            Real.exp (-(t * semiDegeneratePotential lam z))) =
-        (fun z : ℝ × ℝ =>
-          (z.1 ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential z.1))) *
-          (z.2 ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2)))) from by
-        funext z
-        rw [exp_neg_t_semiDegenerate_eq_mul lam t z]
-        ring]
-  exact MeasureTheory.integral_prod_mul
-    (f := fun x : ℝ => x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x)))
-    (g := fun y : ℝ => y ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam y)))
+  simp only [semiDegeneratePotential_eq_addSeparable]
+  exact integral_separable_addSeparable _ _ _ (fun x => x ^ m) (fun y => y ^ n)
 
 /-! ## Specialised moments needed for affine covariance -/