The atoms of the configuration energy

For a configuration t : Fin h → ℝ and a radius ε > 0, the atoms are the circles of radius ε around the t i (weights 1/K) and the sixteen arcsine curves (weights -c_j). This file verifies the hypotheses of energy_log_nonpos for these atoms.

theorem Zeta5Irrational.sum_Icc_eq_sum_range' (m : ℕ) (f : ℕ → ℝ) : ∑ j ∈ Finset.Icc 1 m, f j = ∑ j ∈ Finset.range m, f (j + 1)

Reindexing ∑_{j ∈ Icc 1 m} f j = ∑_{j < m} f (j + 1).

noncomputable def Zeta5Irrational.mρ (j : ℕ) : ℝ

Midpoints and half-lengths of the intervals of Table 1.

Equations

• Zeta5Irrational.mρ j = (Zeta5Irrational.aρ j + Zeta5Irrational.bρ j) / 2

noncomputable def Zeta5Irrational.rρ (j : ℕ) : ℝ

Half-width of the support of the jth arcsine component.

Equations

• Zeta5Irrational.rρ j = (Zeta5Irrational.bρ j - Zeta5Irrational.aρ j) / 2

theorem Zeta5Irrational.rρ_pos (j : Fin 16) : 0 < rρ (↑j + 1)

theorem Zeta5Irrational.rρ_ge (j : Fin 16) : 1 / 450 ≤ rρ (↑j + 1)

theorem Zeta5Irrational.mρ_bounds (j : Fin 16) : 0 < mρ (↑j + 1) ∧ mρ (↑j + 1) < 2

theorem Zeta5Irrational.rρ_le (j : Fin 16) : rρ (↑j + 1) ≤ 1

@[reducible, inline]

abbrev Zeta5Irrational.Idx (h : ℕ) : Type

The index type of the atoms.

Equations

• Zeta5Irrational.Idx h = (Fin h ⊕ Fin 16)

noncomputable def Zeta5Irrational.atomS (h : ℕ) (K : ℝ) : Idx h → ℝ

The weights.

Equations

• Zeta5Irrational.atomS h K (Sum.inl val) = 1 / K
• Zeta5Irrational.atomS h K (Sum.inr j) = -Zeta5Irrational.cρ (↑j + 1)

noncomputable def Zeta5Irrational.atomγ {h : ℕ} (t : Fin h → ℝ) (ε : ℝ) : Idx h → ℝ → ℂ

The curves.

Equations

• Zeta5Irrational.atomγ t ε (Sum.inl val) = circleMap (↑(t val)) ε
• Zeta5Irrational.atomγ t ε (Sum.inr j) = Zeta5Irrational.arcCurve (Zeta5Irrational.mρ (↑j + 1)) (Zeta5Irrational.rρ (↑j + 1))

theorem Zeta5Irrational.continuous_atomγ {h : ℕ} (t : Fin h → ℝ) (ε : ℝ) (k : Idx h) : Continuous (atomγ t ε k)

theorem Zeta5Irrational.norm_atomγ_le {h : ℕ} (t : Fin h → ℝ) (ε : ℝ) (k : Idx h) (θ : ℝ) : ‖atomγ t ε k θ‖ ≤ ∑ i : Fin h, |t i| + |ε| + 3

theorem Zeta5Irrational.atomS_mass (n : ℕ) (hn : 0 < n) : ∑ k : Idx (37 * n), atomS (37 * n) (Kr n) k = 0

Zero total mass when h = 37 n and K = 40 n.

Pointwise integrability and bounds for the atoms

theorem Zeta5Irrational.circle_point_abs_log_le (z c : ℂ) {ε : ℝ} (hε : 0 < ε) : ∫ (φ : ℝ) in 0..2 * Real.pi, |Real.log ‖z - circleMap c ε φ‖| ≤ 2 * Real.pi * |Real.log ε| + 4 * Real.pi * Real.log (1 + ‖(z - c) / ↑ε‖)

∫₀^{2π} |log ‖z - circleMap c ε φ‖| ≤ 2π |log ε| + 4π log (1 + ‖(z - c)/ε‖).

theorem Zeta5Irrational.atom_point_integrable {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (_hε : 0 < ε) (k : Idx h) (z : ℂ) : IntervalIntegrable (fun (φ : ℝ) => Real.log ‖z - atomγ t ε k φ‖) MeasureTheory.volume 0 (2 * Real.pi)

Integrability of φ ↦ log ‖z - atomγ k φ‖.

theorem Zeta5Irrational.norm_root_le {ζ sq : ℂ} (hsq : sq ^ 2 = ζ ^ 2 - 1) : ‖sq‖ ≤ ‖ζ‖ + 1

theorem Zeta5Irrational.atom_point_abs_log_le {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (k : Idx h) {R : ℝ} (_hR : 0 ≤ R) : ∃ (C : ℝ), ∀ (z : ℂ), ‖z‖ ≤ R → ∫ (φ : ℝ) in 0..2 * Real.pi, |Real.log ‖z - atomγ t ε k φ‖| ≤ C

A uniform bound for ∫₀^{2π} |log ‖z - atomγ k φ‖| dφ over ‖z‖ ≤ R.

The hypotheses of energy_log_nonpos

theorem Zeta5Irrational.measurable_atom_kernel {h : ℕ} (t : Fin h → ℝ) (ε : ℝ) (k l : Idx h) : Measurable fun (p : ℝ × ℝ) => Real.log ‖atomγ t ε k p.1 - atomγ t ε l p.2‖

theorem Zeta5Irrational.atom_pair_integrable {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (k l : Idx h) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => Real.log ‖atomγ t ε k p.1 - atomγ t ε l p.2‖) (μcirc.prod μcirc)

Torus integrability of the logarithmic kernel for each pair of atoms.

theorem Zeta5Irrational.atom_preimage_countable {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (l : Idx h) (c : ℂ) : {φ : ℝ | c = atomγ t ε l φ}.Countable

Point preimages under the atoms are countable.

theorem Zeta5Irrational.atom_pair_ae_ne {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (k l : Idx h) : ∀ᵐ (p : ℝ × ℝ) ∂μcirc.prod μcirc, atomγ t ε k p.1 ≠ atomγ t ε l p.2

Almost every pair of parameters gives distinct points.

theorem Zeta5Irrational.pairInt_log_symm {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (k l : Idx h) : pairInt (atomγ t ε) (fun (z w : ℂ) => Real.log ‖z - w‖) k l = pairInt (atomγ t ε) (fun (z w : ℂ) => Real.log ‖z - w‖) l k

Symmetry of the pair integrals of the logarithmic kernel.

theorem Zeta5Irrational.atom_energy_nonpos (n : ℕ) (hn : 0 < n) (t : Fin (37 * n) → ℝ) {ε : ℝ} (hε : 0 < ε) : (energy (atomS (37 * n) (Kr n)) (atomγ t ε) fun (z w : ℂ) => Real.log ‖z - w‖) ≤ 0

Lemma 6.2 for the configuration atoms.