Revert "Merge pull request #35 from or4nge19/3D-Neural-Network"

GibbsMeasure/SpinGlass.lean

@@ -18,36 +18,46 @@ instance : MeasurableSpace Int := ⊤
 /-- The Sherrington-Kirkpatrick (or Edwards-Anderson) potential.
     Φ_{ij}(σ) = - J_{ij} * σ_i * σ_j.
     (Using -J for ferromagnetic convention, or just J). -/
-noncomputable def skPotential (J : V → V → ℝ) : Potential V Int :=
+def skPotential (J : V → V → ℝ) : Potential V Int :=
   fun Δ σ ↦
     if h : ∃ i j, i ≠ j ∧ Δ = {i, j} then
-      -- Use classical choice to extract witnesses from `∃` (cannot eliminate `Exists` into `ℝ` directly).
-      let i : V := Classical.choose h;
-      let hj : ∃ j : V, i ≠ j ∧ Δ = {i, j} := Classical.choose_spec h;
-      let j : V := Classical.choose hj;
+      let ⟨i, j, _⟩ := h
+      -- We need to be careful with double counting if {i,j} = {j,i}.
+      -- The potential is defined on the set Δ.
+      -- J should be symmetric.
       - J i j * (σ i : ℝ) * (σ j : ℝ)
-    else 0
+    else
+      0
 
 instance (J : V → V → ℝ) : Potential.IsFinitary (skPotential J) where
   finite_support := by
-    classical
-    -- Since `V` is finite, the type `Finset V` is finite, hence any subset is finite.
-    exact (Set.finite_univ.subset (by intro Δ hΔ; trivial))
+    let s : Finset (Finset V) := Finset.univ.biUnion fun i ↦ Finset.univ.map ⟨fun j ↦ {i, j}, by simp⟩
+    apply Set.Finite.subset (s := (s : Set (Finset V)))
+    · exact Finset.finite_toSet s
+    · intro Δ hΔ
+      simp only [skPotential, ne_eq, Set.mem_setOf_eq] at hΔ
+      split at hΔ
+      · obtain ⟨i, j, _, rfl⟩ := ‹∃ i j, i ≠ j ∧ Δ = {i, j}›
+        simp [s]
+      · contradiction
 
 instance (J : V → V → ℝ) : Potential.IsPotential (skPotential J) where
   measurable Δ := by
-    classical
-    -- With `MeasurableSpace Int := ⊤`, the induced measurable space on configurations is `⊤`,
-    -- so every function is measurable.
-    intro s hs
-    -- `cylinderEvents` is a comap of a restriction map; comap of `⊤` is `⊤`, hence all sets are measurable.
-    simp [cylinderEvents_eq_comap_restrict]
+    simp only [skPotential]
+    split_ifs with h
+    · obtain ⟨i, j, _, rfl⟩ := h
+      apply Measurable.mul
+      · apply Measurable.mul
+        · exact measurable_const
+        · exact (measurable_from_top.comp (measurable_cylinderEvent_apply (i := i) (X := fun _ : V ↦ Int) (by simp)))
+      · exact (measurable_from_top.comp (measurable_cylinderEvent_apply (i := j) (X := fun _ : V ↦ Int) (by simp)))
+    · exact measurable_const
 
 /-- The Gibbs specification for the SK model. -/
 noncomputable def skSpecification (J : V → V → ℝ) (β : ℝ) (ν : Measure Int)
     [IsProbabilityMeasure ν]
     (hZ : ∀ (Λ : Finset V) (η : V → Int),
-      Specification.premodifierZ ν (Potential.boltzmannWeight (Φ := skPotential J) β) Λ η ≠ ⊤) :
+      Specification.premodifierZ ν (Potential.boltzmannWeight (skPotential J) β) Λ η ≠ ⊤) :
     Specification V Int :=
   Potential.gibbsSpecification (skPotential J) β ν hZ
 

MCMC/Finite/Convergence.lean

@@ -461,66 +461,6 @@ lemma distribution_converges_to_stationarity [Nonempty n]
       _ = π.val i := by simp [h_one]
   simpa [h_left, h_right] using h_sum
 
-/-! #### (B) Convergence in total variation -/
-
-lemma tvDist_row_converges_to_stationary [Nonempty n]
-    (P : Matrix n n ℝ) (π : stdSimplex ℝ n) (hMCMC : IsMCMC P π) (i : n) :
-    Tendsto (fun k : ℕ => Matrix.tvDist (Matrix.rowDist (P^k) i) π.val) atTop (𝓝 0) := by
-  classical
-  have h_conv : Tendsto (fun k : ℕ => P ^ k) atTop (𝓝 (LimitMatrix π)) :=
-    convergence_to_stationarity P π hMCMC
-  -- pointwise convergence of entries in row `i`
-  have h_abs (j : n) :
-      Tendsto (fun k : ℕ => |(P^k) i j - π.val j|) atTop (𝓝 (0 : ℝ)) := by
-    have h_entry :
-        Tendsto (fun k : ℕ => (P ^ k) i j) atTop (𝓝 (LimitMatrix π i j)) := by
-      have h_eval : Continuous fun M : Matrix n n ℝ => M i j := by
-        simpa using ((continuous_apply j).comp (continuous_apply i))
-      exact (h_eval.tendsto _).comp h_conv
-    have h_diff :
-        Tendsto (fun k : ℕ => (P ^ k) i j - π.val j) atTop (𝓝 (0 : ℝ)) := by
-      -- `LimitMatrix π i j = π.val j`
-      have : Tendsto (fun k : ℕ => (P ^ k) i j - π.val j) atTop
-          (𝓝 (LimitMatrix π i j - π.val j)) := h_entry.sub tendsto_const_nhds
-      simpa [LimitMatrix] using this
-    -- continuity of `abs`
-    simpa using (continuous_abs.tendsto (0 : ℝ)).comp h_diff
-  have h_sum :
-      Tendsto (fun k : ℕ => ∑ j, |(P^k) i j - π.val j|) atTop (𝓝 (0 : ℝ)) := by
-    simpa using
-      (tendsto_finset_sum (s := (Finset.univ : Finset n))
-        (fun j _ => h_abs j))
-  -- divide by 2 to get TV
-  have : Tendsto (fun k : ℕ => (∑ j, |(P^k) i j - π.val j|) / 2) atTop (𝓝 (0 : ℝ)) := by
-    simpa using h_sum.div_const (2 : ℝ)
-  simpa [Matrix.tvDist, Matrix.rowDist] using this
-
-lemma tvDist_distributionAtTime_converges_to_stationary [Nonempty n]
-    (P : Matrix n n ℝ) (π : stdSimplex ℝ n) (hMCMC : IsMCMC P π)
-    (μ₀ : stdSimplex ℝ n) :
-    Tendsto (fun k : ℕ => Matrix.tvDist (distributionAtTime P μ₀ k) π.val) atTop (𝓝 0) := by
-  classical
-  have hμ : Tendsto (distributionAtTime P μ₀) atTop (𝓝 π.val) :=
-    distribution_converges_to_stationarity P π hMCMC μ₀
-  have h_abs (i : n) :
-      Tendsto (fun k : ℕ => |distributionAtTime P μ₀ k i - π.val i|) atTop (𝓝 (0 : ℝ)) := by
-    have h_diff :
-        Tendsto (fun k : ℕ => distributionAtTime P μ₀ k i - π.val i) atTop (𝓝 (0 : ℝ)) := by
-      have : Tendsto (fun k : ℕ => distributionAtTime P μ₀ k i - π.val i) atTop
-          (𝓝 (π.val i - π.val i)) :=
-        (tendsto_pi_nhds.mp hμ i).sub tendsto_const_nhds
-      simpa using this
-    -- continuity of `abs`
-    simpa using (continuous_abs.tendsto (0 : ℝ)).comp h_diff
-  have h_sum :
-      Tendsto (fun k : ℕ => ∑ i, |distributionAtTime P μ₀ k i - π.val i|) atTop (𝓝 (0 : ℝ)) := by
-    simpa using
-      (tendsto_finset_sum (s := (Finset.univ : Finset n))
-        (fun i _ => h_abs i))
-  have : Tendsto (fun k : ℕ => (∑ i, |distributionAtTime P μ₀ k i - π.val i|) / 2) atTop (𝓝 (0 : ℝ)) := by
-    simpa using h_sum.div_const (2 : ℝ)
-  simpa [Matrix.tvDist] using this
-
 /-! #### The Ergodic Theorem (Law of Large Numbers) -/
 
 /-- Expectation of a function f under a distribution π. E_π[f]. -/

MCMC/Finite/toKernel.lean

@@ -202,26 +202,6 @@ theorem isStationary_iff_invariant (P : Matrix n n ℝ) (π : stdSimplex ℝ n)
     simpa [IsStationary, Matrix.mulVec, dotProduct, Matrix.transpose,
            Matrix.transpose_apply] using hcoord j
 
-/-!
-### (A) Finite-state existence/uniqueness of invariant measure
-
-We expose the Perron–Frobenius existence/uniqueness theorem (proved in `MCMC.Finite.Core` for the
-simplex) as a statement about `Kernel.Invariant` for the associated kernel on the finite space.
--/
-
-theorem exists_unique_invariant_measure_of_irreducible
-    [Nonempty n] {P : Matrix n n ℝ} (hP : IsStochastic P) (h_irred : Matrix.IsIrreducible P) :
-    ∃! (π : stdSimplex ℝ n),
-      Kernel.Invariant (matrixToKernel P hP) (vecToMeasure π) := by
-  classical
-  obtain ⟨π, hπ_stat, hπ_unique⟩ :=
-    exists_unique_stationary_distribution_of_irreducible (n := n) (P := P) hP h_irred
-  refine ⟨π, (isStationary_iff_invariant (n := n) (P := P) (π := π) hP).1 hπ_stat, ?_⟩
-  intro π' hπ'_inv
-  have hπ'_stat : IsStationary P π' :=
-    (isStationary_iff_invariant (n := n) (P := P) (π := π') hP).2 hπ'_inv
-  exact hπ_unique π' hπ'_stat
-
 /-- Matrix reversibility is equivalent to kernel reversibility -/
 theorem isReversible_iff_kernel_reversible (P : Matrix n n ℝ) (π : stdSimplex ℝ n)
     (hP : IsStochastic P) :
@@ -419,9 +399,9 @@ theorem isReversible_iff_kernel_reversible (P : Matrix n n ℝ) (π : stdSimplex
           ∫⁻ x in ({i} : Set n), κ x {j} ∂μ
             = ∑ k : n, ENNReal.ofReal (π.val k) *
                 (({i} : Set n).indicator (fun x => κ x {j}) k) := by
-        rw [← lintegral_indicator (μ := μ) (s := ({i} : Set n))
-              (f := fun x => κ x {j}) hAi]
         simp [μ, vecToMeasure]
+        ring_nf
+        simp [Set.indicator_apply]
       have hsum :
           ∑ k : n, ENNReal.ofReal (π.val k) *
               (({i} : Set n).indicator (fun x => κ x {j}) k)
@@ -440,9 +420,9 @@ theorem isReversible_iff_kernel_reversible (P : Matrix n n ℝ) (π : stdSimplex
           ∫⁻ x in ({j} : Set n), κ x {i} ∂μ
             = ∑ k : n, ENNReal.ofReal (π.val k) *
                 (({j} : Set n).indicator (fun x => κ x {i}) k) := by
-        rw [← lintegral_indicator (μ := μ) (s := ({j} : Set n))
-              (f := fun x => κ x {i}) hBj]
         simp [μ, vecToMeasure]
+        ring_nf
+        simp [Set.indicator_apply]
       have hsum :
           ∑ k : n, ENNReal.ofReal (π.val k) *
               (({j} : Set n).indicator (fun x => κ x {i}) k)