Skip to content

feat: §18.6 mayerPartialSum tanh β/J 4-layer wraps (32 thm) — #1344 #1583

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
phasetr merged 3 commits into from
May 4, 2026
Merged

feat: §18.6 mayerPartialSum tanh β/J 4-layer wraps (32 thm) — #1344 #1583

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0ae96d5
chore: open §18.6 mayerPartialSum tanh β/J 4-layer bundle PR (Part of…
phasetr May 4, 2026
80d4402
feat: §18.6 mayerPartialSum tanh β/J 4-layer wraps (32 thm)
phasetr May 4, 2026
3bf52e3
docs: fix tex/proof-guide.tex §18.6 → §18.5 section label per codex f…
phasetr May 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 76 additions & 0 deletions IsingModel/AmbientLattice/Analyticity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -848,5 +848,81 @@ theorem mayerExpansionTerm_Λ_analyticOnNhd
Set.univ :=
IsingModel.mayerExpansionTerm_analyticOnNhd (inducedGraph G Λ) n

/-! ### §18.6 mayerPartialSum tanh β/J Λ wraps -/

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (·*J)` continuous in β**. -/
theorem mayerPartialSum_Λ_tanh_continuous_beta
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (J : ℝ) :
Continuous (fun β' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β' * J))) :=
IsingModel.mayerPartialSum_tanh_continuous_beta (inducedGraph G Λ) N J

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (β*·)` continuous in J**. -/
theorem mayerPartialSum_Λ_tanh_continuous_J
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (β : ℝ) :
Continuous (fun J' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β * J'))) :=
IsingModel.mayerPartialSum_tanh_continuous_J (inducedGraph G Λ) N β

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (·*J)` differentiable in β**. -/
theorem mayerPartialSum_Λ_tanh_differentiable_beta
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (J : ℝ) :
Differentiable ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β' * J))) :=
IsingModel.mayerPartialSum_tanh_differentiable_beta (inducedGraph G Λ) N J

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (β*·)` differentiable in J**. -/
theorem mayerPartialSum_Λ_tanh_differentiable_J
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (β : ℝ) :
Differentiable ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β * J'))) :=
IsingModel.mayerPartialSum_tanh_differentiable_J (inducedGraph G Λ) N β

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (·*J)` AnalyticAt in β**. -/
theorem mayerPartialSum_Λ_tanh_analyticAt_beta
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (J β : ℝ) :
AnalyticAt ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β' * J))) β :=
IsingModel.mayerPartialSum_tanh_analyticAt_beta (inducedGraph G Λ) N J β

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (β*·)` AnalyticAt in J**. -/
theorem mayerPartialSum_Λ_tanh_analyticAt_J
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (β J : ℝ) :
AnalyticAt ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β * J'))) J :=
IsingModel.mayerPartialSum_tanh_analyticAt_J (inducedGraph G Λ) N β J

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (·*J)` AnalyticOnNhd in β
over `Set.univ`**. -/
theorem mayerPartialSum_Λ_tanh_analyticOnNhd_beta
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (J : ℝ) :
AnalyticOnNhd ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β' * J))) Set.univ :=
IsingModel.mayerPartialSum_tanh_analyticOnNhd_beta (inducedGraph G Λ) N J

/-- **Λ-layer: `mayerPartialSum ∘ tanh ∘ (β*·)` AnalyticOnNhd in J
over `Set.univ`**. -/
theorem mayerPartialSum_Λ_tanh_analyticOnNhd_J
(G : SimpleGraph V) (Λ : Finset V)
[Fintype (inducedGraph G Λ).edgeSet] (N : ℕ) (β : ℝ) :
AnalyticOnNhd ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum (inducedGraph G Λ) N
(Real.tanh (β * J'))) Set.univ :=
IsingModel.mayerPartialSum_tanh_analyticOnNhd_J (inducedGraph G Λ) N β

end Ambient
end IsingModel
92 changes: 92 additions & 0 deletions IsingModel/AmbientLattice/SpecialCases.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3251,5 +3251,97 @@ theorem mayerExpansionTermAlongExhaustion_analyticOnNhd
(inducedGraph G (Λ.volume n)) k s) Set.univ :=
mayerExpansionTerm_Λ_analyticOnNhd G (Λ.volume n) k

/-! ### §18.6 mayerPartialSum tanh β/J along-ex wraps -/

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (·*J) continuous in β**. -/
theorem mayerPartialSumAlongExhaustion_tanh_continuous_beta
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
Continuous (fun β' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β' * J))) :=
mayerPartialSum_Λ_tanh_continuous_beta G (Λ.volume n) N J

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (β*·) continuous in J**. -/
theorem mayerPartialSumAlongExhaustion_tanh_continuous_J
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
Continuous (fun J' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β * J'))) :=
mayerPartialSum_Λ_tanh_continuous_J G (Λ.volume n) N β

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (·*J) differentiable in β**. -/
theorem mayerPartialSumAlongExhaustion_tanh_differentiable_beta
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
Differentiable ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β' * J))) :=
mayerPartialSum_Λ_tanh_differentiable_beta G (Λ.volume n) N J

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (β*·) differentiable in J**. -/
theorem mayerPartialSumAlongExhaustion_tanh_differentiable_J
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
Differentiable ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β * J'))) :=
mayerPartialSum_Λ_tanh_differentiable_J G (Λ.volume n) N β

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticAt in β**. -/
theorem mayerPartialSumAlongExhaustion_tanh_analyticAt_beta
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (J β : ℝ) (n : ℕ) :
AnalyticAt ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β' * J))) β :=
mayerPartialSum_Λ_tanh_analyticAt_beta G (Λ.volume n) N J β

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticAt in J**. -/
theorem mayerPartialSumAlongExhaustion_tanh_analyticAt_J
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (β J : ℝ) (n : ℕ) :
AnalyticAt ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β * J'))) J :=
mayerPartialSum_Λ_tanh_analyticAt_J G (Λ.volume n) N β J

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticOnNhd in β
over `Set.univ`**. -/
theorem mayerPartialSumAlongExhaustion_tanh_analyticOnNhd_beta
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
AnalyticOnNhd ℝ (fun β' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β' * J))) Set.univ :=
mayerPartialSum_Λ_tanh_analyticOnNhd_beta G (Λ.volume n) N J

/-- **Along-ex: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticOnNhd in J
over `Set.univ`**. -/
theorem mayerPartialSumAlongExhaustion_tanh_analyticOnNhd_J
(G : SimpleGraph V) (Λ : Exhaustion V)
[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
AnalyticOnNhd ℝ (fun J' : ℝ =>
IsingModel.mayerPartialSum
(inducedGraph G (Λ.volume n)) N
(Real.tanh (β * J'))) Set.univ :=
mayerPartialSum_Λ_tanh_analyticOnNhd_J G (Λ.volume n) N β

end Ambient
end IsingModel
192 changes: 192 additions & 0 deletions IsingModel/Concrete/LatticeGraphCorrelation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8940,6 +8940,198 @@ theorem mayerExpansionTermAlongExhaustion_latticeGraph_analyticOnNhd
Ambient.mayerExpansionTermAlongExhaustion_analyticOnNhd
(IsingModel.latticeGraph d) Λ k n

/-! ### §18.6 mayerPartialSum tanh β/J ℤ^d wraps -/

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (·*J) continuous in β**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_continuous_beta
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (J : ℝ) :
Continuous (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β' * J))) :=
Ambient.mayerPartialSum_Λ_tanh_continuous_beta
(IsingModel.latticeGraph d) Λ N J

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (β*·) continuous in J**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_continuous_J
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (β : ℝ) :
Continuous (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β * J'))) :=
Ambient.mayerPartialSum_Λ_tanh_continuous_J
(IsingModel.latticeGraph d) Λ N β

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (·*J) differentiable in β**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_differentiable_beta
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (J : ℝ) :
Differentiable ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β' * J))) :=
Ambient.mayerPartialSum_Λ_tanh_differentiable_beta
(IsingModel.latticeGraph d) Λ N J

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (β*·) differentiable in J**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_differentiable_J
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (β : ℝ) :
Differentiable ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β * J'))) :=
Ambient.mayerPartialSum_Λ_tanh_differentiable_J
(IsingModel.latticeGraph d) Λ N β

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticAt in β**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_analyticAt_beta
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (J β : ℝ) :
AnalyticAt ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β' * J))) β :=
Ambient.mayerPartialSum_Λ_tanh_analyticAt_beta
(IsingModel.latticeGraph d) Λ N J β

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticAt in J**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_analyticAt_J
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (β J : ℝ) :
AnalyticAt ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β * J'))) J :=
Ambient.mayerPartialSum_Λ_tanh_analyticAt_J
(IsingModel.latticeGraph d) Λ N β J

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticOnNhd Set.univ
in β**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_analyticOnNhd_beta
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (J : ℝ) :
AnalyticOnNhd ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β' * J))) Set.univ :=
Ambient.mayerPartialSum_Λ_tanh_analyticOnNhd_beta
(IsingModel.latticeGraph d) Λ N J

/-- **ℤ^d Λ: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticOnNhd Set.univ
in J**. -/
theorem mayerPartialSum_Λ_latticeGraph_tanh_analyticOnNhd_J
(d : ℕ) (Λ : Finset (Fin d → ℤ))
[Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet]
(N : ℕ) (β : ℝ) :
AnalyticOnNhd ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) Λ) N
(Real.tanh (β * J'))) Set.univ :=
Ambient.mayerPartialSum_Λ_tanh_analyticOnNhd_J
(IsingModel.latticeGraph d) Λ N β

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (·*J) continuous in β**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_continuous_beta
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
Continuous (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β' * J))) :=
Ambient.mayerPartialSumAlongExhaustion_tanh_continuous_beta
(IsingModel.latticeGraph d) Λ N J n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (β*·) continuous in J**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_continuous_J
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
Continuous (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β * J'))) :=
Ambient.mayerPartialSumAlongExhaustion_tanh_continuous_J
(IsingModel.latticeGraph d) Λ N β n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (·*J) differentiable in β**. -/
theorem
mayerPartialSumAlongExhaustion_latticeGraph_tanh_differentiable_beta
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
Differentiable ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β' * J))) :=
Ambient.mayerPartialSumAlongExhaustion_tanh_differentiable_beta
(IsingModel.latticeGraph d) Λ N J n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (β*·) differentiable in J**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_differentiable_J
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
Differentiable ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β * J'))) :=
Ambient.mayerPartialSumAlongExhaustion_tanh_differentiable_J
(IsingModel.latticeGraph d) Λ N β n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticAt in β**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_analyticAt_beta
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (J β : ℝ) (n : ℕ) :
AnalyticAt ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β' * J))) β :=
Ambient.mayerPartialSumAlongExhaustion_tanh_analyticAt_beta
(IsingModel.latticeGraph d) Λ N J β n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticAt in J**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_analyticAt_J
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (β J : ℝ) (n : ℕ) :
AnalyticAt ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β * J'))) J :=
Ambient.mayerPartialSumAlongExhaustion_tanh_analyticAt_J
(IsingModel.latticeGraph d) Λ N β J n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (·*J) AnalyticOnNhd
Set.univ in β**. -/
theorem
mayerPartialSumAlongExhaustion_latticeGraph_tanh_analyticOnNhd_beta
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (J : ℝ) (n : ℕ) :
AnalyticOnNhd ℝ (fun β' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β' * J))) Set.univ :=
Ambient.mayerPartialSumAlongExhaustion_tanh_analyticOnNhd_beta
(IsingModel.latticeGraph d) Λ N J n

/-- **ℤ^d along-ex: mayerPartialSum ∘ tanh ∘ (β*·) AnalyticOnNhd
Set.univ in J**. -/
theorem mayerPartialSumAlongExhaustion_latticeGraph_tanh_analyticOnNhd_J
(d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ))
[∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d)
(Λ.volume n)).edgeSet]
(N : ℕ) (β : ℝ) (n : ℕ) :
AnalyticOnNhd ℝ (fun J' : ℝ => IsingModel.mayerPartialSum
(inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)) N
(Real.tanh (β * J'))) Set.univ :=
Ambient.mayerPartialSumAlongExhaustion_tanh_analyticOnNhd_J
(IsingModel.latticeGraph d) Λ N β n

end Ambient

end IsingModel
2 changes: 1 addition & 1 deletion docs/index.md
View file
Open in desktop

Large diffs are not rendered by default.

10 changes: 10 additions & 0 deletions tex/proof-guide.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3489,6 +3489,16 @@ \section{Cluster (polymer / Mayer) expansion (\S18.4--\S18.7)}
\texttt{\_ferro} (instead of \texttt{\_ferromagnetic}) so each
declaration fits the linter's 100-character budget.

\paragraph{\texttt{mayerPartialSum} $\beta$ / $J$ regularity (tanh
form), all volume layers (\S18.5, PR~\#1583).} The eight abstract
$\beta$/$J$ regularity statements (continuous, differentiable,
analyticAt, analyticOnNhd, each in $\beta$ and $J$) for
\texttt{mayerPartialSum} composed with $\tanh(\beta J)$ are lifted
to the four volume layers, giving $32$ thin direct-instantiation
wrappers in \texttt{IsingModel/AmbientLattice/Analyticity.lean},
\texttt{AmbientLattice/SpecialCases.lean}, and
\texttt{Concrete/LatticeGraphCorrelation.lean}.

\paragraph{\texttt{mayerExpansionTerm} regularity, all volume layers
(\S18.6, PR~\#1582).} The four abstract regularity statements
(\texttt{mayerExpansionTerm\_continuous} (Step~588),
Expand Down