mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
fix(lean): complete N3L_Energy.lean build — fix rcases shadowing, fraction addition, linarith with ∀ quantifier
- Fix rcases (rfl|rfl|rfl) shadowing by using named patterns hl_i/hl_j/hl_m with rw - Fix fraction addition calc block: replace simp with field_simp + ring - Fix linarith failures: extract specific hm_i/hm_j/hm_m from ∀ hmass - 3 original sorries preserved (peak_integrable_over_R, signedArea_zero_implies_perpDist_zero, no_collinear_at_zero_energy) Build: 8587 jobs, 0 errors (lake build Semantics)
This commit is contained in:
parent
2c53cf45ca
commit
1d6b0fe5e0
2 changed files with 546 additions and 0 deletions
|
|
@ -213,6 +213,7 @@ import Semantics.CGAVersorAddress
|
|||
import Semantics.FAMMCoChain
|
||||
import Semantics.NKHodgeFAMM
|
||||
import Semantics.Goxel
|
||||
import Semantics.N3L_Energy
|
||||
|
||||
namespace Semantics
|
||||
|
||||
|
|
|
|||
545
0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean
Normal file
545
0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean
Normal file
|
|
@ -0,0 +1,545 @@
|
|||
/-
|
||||
N3L_Energy.lean — No-Three-in-Line energy rigidity theorem
|
||||
|
||||
Formalizes the energy-minimization approach to the
|
||||
No-Three-in-Line problem in ℝ² with Gaussian ansatz.
|
||||
|
||||
Main result: no_collinear_at_zero_energy
|
||||
E = 0 (energy of all lines) ⇒ no three peaks collinear
|
||||
-/
|
||||
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.Analysis.SpecialFunctions.Exp
|
||||
import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
|
||||
import Mathlib.MeasureTheory.Integral.Bochner.Basic
|
||||
import Mathlib.Data.Finset.Basic
|
||||
import Mathlib.Tactic
|
||||
|
||||
open Real MeasureTheory Finset
|
||||
|
||||
namespace Semantics.N3L_Energy
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §0 CORE DEFINITIONS
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
noncomputable def gaussian2D (σ m : ℝ) (x : ℝ × ℝ) : ℝ :=
|
||||
m / (2 * π * σ ^ 2) * Real.exp (-(x.1 ^ 2 + x.2 ^ 2) / (2 * σ ^ 2))
|
||||
|
||||
noncomputable def gaussianAnsatz_eval (σ : ℝ) {k : ℕ}
|
||||
(positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) (x : ℝ × ℝ) : ℝ :=
|
||||
(Finset.univ : Finset (Fin k)).sum (fun i =>
|
||||
gaussian2D σ (masses i) (x.1 - (positions i).1, x.2 - (positions i).2))
|
||||
|
||||
noncomputable def penalty (lam z : ℝ) : ℝ :=
|
||||
if z > 0 then lam * z ^ 2 else 0
|
||||
|
||||
noncomputable def σ_crit : ℝ := 3 / (2 * Real.sqrt (2 * π))
|
||||
|
||||
def signedArea (p₁ p₂ p₃ : ℝ × ℝ) : ℝ :=
|
||||
(p₂.1 - p₁.1) * (p₃.2 - p₁.2) - (p₃.1 - p₁.1) * (p₂.2 - p₁.2)
|
||||
|
||||
def perpDistance (x₀ y₀ a b s t : ℝ) : ℝ :=
|
||||
|a * (t - y₀) - b * (s - x₀)|
|
||||
|
||||
noncomputable def ansatzLineDensity (σ : ℝ) {k : ℕ}
|
||||
(positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ)
|
||||
(a b s t : ℝ) : ℝ :=
|
||||
∫ τ : ℝ, gaussianAnsatz_eval σ positions masses (s + a * τ, t + b * τ)
|
||||
|
||||
noncomputable def energy {ι : Type*} [Fintype ι] [DecidableEq ι]
|
||||
(lam : ℝ) (densities : ι → ℝ) : ℝ :=
|
||||
Finset.univ.sum (fun i => penalty lam (densities i - 2))
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §1 GAUSSIAN INTEGRAL
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
lemma integral_comp_add_right_ℝ (f : ℝ → ℝ) (x₀ : ℝ) :
|
||||
(∫ τ : ℝ, f (τ - x₀)) = (∫ u : ℝ, f u) := by
|
||||
have hp : MeasurePreserving (fun τ : ℝ => τ - x₀) volume volume := by
|
||||
simpa [sub_eq_add_neg] using measurePreserving_add_right volume (-x₀)
|
||||
have hembed : MeasurableEmbedding (fun τ : ℝ => τ - x₀) := by
|
||||
simpa [sub_eq_add_neg, add_comm] using measurableEmbedding_addLeft (-x₀)
|
||||
simpa using (hp.integral_comp hembed f)
|
||||
|
||||
theorem integral_gaussian_1d (σ : ℝ) (hσ : σ > 0) :
|
||||
(∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) = σ * Real.sqrt (2 * π) := by
|
||||
have hg := integral_gaussian (1 / (2 * σ ^ 2))
|
||||
have h_eq : (∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) =
|
||||
(∫ t : ℝ, Real.exp (-(1 / (2 * σ ^ 2)) * t ^ 2)) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with t; apply congrArg Real.exp; field_simp [hσ.ne.symm]
|
||||
rw [h_eq, hg]
|
||||
calc
|
||||
Real.sqrt (π / (1 / (2 * σ ^ 2))) = Real.sqrt (π * (2 * σ ^ 2)) := by
|
||||
field_simp [hσ.ne.symm]
|
||||
_ = Real.sqrt ((σ ^ 2) * (2 * π)) := by
|
||||
apply congrArg Real.sqrt; ring
|
||||
_ = Real.sqrt (σ ^ 2) * Real.sqrt (2 * π) := by rw [Real.sqrt_mul (sq_nonneg σ)]
|
||||
_ = σ * Real.sqrt (2 * π) := by rw [Real.sqrt_sq (le_of_lt hσ)]
|
||||
|
||||
theorem integral_gaussian_1d_shifted (σ x₀ : ℝ) (hσ : σ > 0) :
|
||||
(∫ t : ℝ, Real.exp (-(t - x₀) ^ 2 / (2 * σ ^ 2))) = σ * Real.sqrt (2 * π) := by
|
||||
calc
|
||||
(∫ t : ℝ, Real.exp (-(t - x₀) ^ 2 / (2 * σ ^ 2)))
|
||||
= (∫ u : ℝ, Real.exp (-u ^ 2 / (2 * σ ^ 2))) :=
|
||||
integral_comp_add_right_ℝ (fun u : ℝ => Real.exp (-u ^ 2 / (2 * σ ^ 2))) x₀
|
||||
_ = (∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with t; field_simp [hσ.ne.symm]
|
||||
_ = σ * Real.sqrt (2 * π) := integral_gaussian_1d σ hσ
|
||||
|
||||
lemma exp_sum_of_sq (t d σ : ℝ) :
|
||||
Real.exp (-(t ^ 2 + d ^ 2) / (2 * σ ^ 2)) =
|
||||
Real.exp (-d ^ 2 / (2 * σ ^ 2)) * Real.exp (-t ^ 2 / (2 * σ ^ 2)) := by
|
||||
rw [← Real.exp_add]; ring_nf
|
||||
|
||||
theorem gaussian_line_integral_at_distance
|
||||
(σ m d : ℝ) (hσ : σ > 0) (hm : m ≥ 0) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (τ, d)) =
|
||||
m / (σ * Real.sqrt (2 * π)) * Real.exp (-d ^ 2 / (2 * σ ^ 2)) := by
|
||||
unfold gaussian2D
|
||||
calc
|
||||
(∫ τ : ℝ, m / (2 * π * σ ^ 2) * Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2)))
|
||||
= m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2))) := by
|
||||
rw [integral_const_mul]
|
||||
_ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) *
|
||||
(∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2)))) := by
|
||||
calc
|
||||
m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2)))
|
||||
= m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-d ^ 2 / (2 * σ ^ 2)) *
|
||||
Real.exp (-τ ^ 2 / (2 * σ ^ 2))) := by
|
||||
refine congrArg (fun t => m / (2 * π * σ ^ 2) * t) ?_
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; exact exp_sum_of_sq τ d σ
|
||||
_ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) *
|
||||
(∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2)))) := by
|
||||
rw [integral_const_mul]
|
||||
_ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) *
|
||||
(σ * Real.sqrt (2 * π))) := by
|
||||
have h_gauss : (∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2))) = σ * Real.sqrt (2 * π) := by
|
||||
calc
|
||||
(∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2))) = (∫ τ : ℝ, Real.exp (-(τ ^ 2 / (2 * σ ^ 2)))) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; apply congrArg Real.exp; field_simp [hσ.ne.symm]
|
||||
_ = σ * Real.sqrt (2 * π) := integral_gaussian_1d σ hσ
|
||||
rw [h_gauss]
|
||||
_ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-d ^ 2 / (2 * σ ^ 2)) := by
|
||||
have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity
|
||||
field_simp [hσ.ne.symm, hs2pi_pos.ne.symm]
|
||||
calc
|
||||
m * Real.sqrt (2 * π) ^ 2 = m * (2 * π) := by
|
||||
rw [Real.sq_sqrt (show 0 ≤ 2 * π by positivity)]
|
||||
_ = m * 2 * π := by ring
|
||||
|
||||
theorem peak_contribution_on_axis
|
||||
(σ m x₀ y₀ t : ℝ) (hσ : σ > 0) (hm : m ≥ 0) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (τ - x₀, t - y₀)) =
|
||||
m / (σ * Real.sqrt (2 * π)) * Real.exp (-(t - y₀) ^ 2 / (2 * σ ^ 2)) := by
|
||||
calc
|
||||
(∫ τ : ℝ, gaussian2D σ m (τ - x₀, t - y₀))
|
||||
= (∫ u : ℝ, gaussian2D σ m (u, t - y₀)) :=
|
||||
integral_comp_add_right_ℝ (fun u : ℝ => gaussian2D σ m (u, t - y₀)) x₀
|
||||
_ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-(t - y₀) ^ 2 / (2 * σ ^ 2)) :=
|
||||
gaussian_line_integral_at_distance σ m (t - y₀) hσ hm
|
||||
|
||||
theorem on_line_contribution
|
||||
(σ m x₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (τ - x₀, 0)) =
|
||||
m / (σ * Real.sqrt (2 * π)) := by
|
||||
calc
|
||||
(∫ τ : ℝ, gaussian2D σ m (τ - x₀, 0))
|
||||
= (∫ u : ℝ, gaussian2D σ m (u, 0)) :=
|
||||
integral_comp_add_right_ℝ (fun u : ℝ => gaussian2D σ m (u, 0)) x₀
|
||||
_ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-(0 : ℝ) ^ 2 / (2 * σ ^ 2)) :=
|
||||
gaussian_line_integral_at_distance σ m 0 hσ hm
|
||||
_ = m / (σ * Real.sqrt (2 * π)) := by norm_num
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §2 PENALTY AND ENERGY
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem penalty_nonneg {lam : ℝ} (hlam : lam ≥ 0) (z : ℝ) : penalty lam z ≥ 0 := by
|
||||
unfold penalty; split_ifs
|
||||
· exact mul_nonneg hlam (sq_nonneg z)
|
||||
· exact le_refl 0
|
||||
|
||||
theorem penalty_zero_iff {lam : ℝ} (hlam : lam > 0) (z : ℝ) : penalty lam z = 0 ↔ z ≤ 0 := by
|
||||
unfold penalty; constructor
|
||||
· intro h; by_contra hz; push_neg at hz
|
||||
rw [if_pos hz] at h
|
||||
have : lam * z ^ 2 > 0 := mul_pos hlam (sq_pos_of_pos hz)
|
||||
linarith
|
||||
· intro h; rw [if_neg (not_lt.mpr h)]
|
||||
|
||||
theorem energy_zero_iff {ι : Type*} [Fintype ι] [DecidableEq ι]
|
||||
{lam : ℝ} (hlam : lam > 0) (densities : ι → ℝ) :
|
||||
energy lam densities = 0 ↔ ∀ j, densities j ≤ 2 := by
|
||||
unfold energy
|
||||
constructor
|
||||
· intro hE j
|
||||
have hterm := (sum_eq_zero_iff_of_nonneg
|
||||
(fun i hi => penalty_nonneg (le_of_lt hlam) (densities i - 2))).mp hE j (Finset.mem_univ j)
|
||||
rw [penalty_zero_iff hlam (densities j - 2)] at hterm
|
||||
exact sub_nonpos.mp hterm
|
||||
· intro hle; apply Finset.sum_eq_zero
|
||||
intro j _; exact (penalty_zero_iff hlam (densities j - 2)).mpr (sub_nonpos.mpr (hle j))
|
||||
|
||||
theorem energy_nonneg {ι : Type*} [Fintype ι] [DecidableEq ι]
|
||||
{lam : ℝ} (hlam : lam ≥ 0) (densities : ι → ℝ) : energy lam densities ≥ 0 :=
|
||||
Finset.sum_nonneg (fun i _ => penalty_nonneg hlam (densities i - 2))
|
||||
|
||||
theorem energy_pos_of_exceeds {ι : Type*} [Fintype ι] [DecidableEq ι]
|
||||
{lam : ℝ} (hlam : lam > 0) {densities : ι → ℝ} {j : ι} (hj : densities j > 2) :
|
||||
energy lam densities > 0 := by
|
||||
have hterm : penalty lam (densities j - 2) > 0 := by
|
||||
by_contra! hle
|
||||
have hzero : penalty lam (densities j - 2) = 0 :=
|
||||
le_antisymm hle (penalty_nonneg (le_of_lt hlam) (densities j - 2))
|
||||
have hdens : densities j - 2 ≤ 0 := ((penalty_zero_iff hlam (densities j - 2)).mp hzero)
|
||||
linarith
|
||||
by_contra hE
|
||||
have hE_nonpos : energy lam densities ≤ 0 := le_of_not_gt hE
|
||||
have h_total_nonneg : energy lam densities ≥ 0 := energy_nonneg (le_of_lt hlam) densities
|
||||
have hE_zero : energy lam densities = 0 := le_antisymm hE_nonpos h_total_nonneg
|
||||
have hall : ∀ k, densities k ≤ 2 := (energy_zero_iff hlam densities).mp hE_zero
|
||||
linarith [hall j, hj]
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §3 THRESHOLD INEQUALITY
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem σ_crit_pos : σ_crit > 0 := by
|
||||
unfold σ_crit; positivity
|
||||
|
||||
theorem three_over_sroot2pi_gt_two
|
||||
{σ : ℝ} (hσ : σ > 0) (hbound : σ < σ_crit) :
|
||||
3 / (σ * Real.sqrt (2 * π)) > 2 := by
|
||||
unfold σ_crit at hbound
|
||||
have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity
|
||||
have hpos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos
|
||||
have hineq : 2 * (σ * Real.sqrt (2 * π)) < 3 := by
|
||||
have hpos2 : (2 : ℝ) * Real.sqrt (2 * π) > 0 := mul_pos (by norm_num) hs2pi_pos
|
||||
calc
|
||||
2 * (σ * Real.sqrt (2 * π)) = (2 * Real.sqrt (2 * π)) * σ := by ring
|
||||
_ < (2 * Real.sqrt (2 * π)) * (3 / (2 * Real.sqrt (2 * π))) :=
|
||||
mul_lt_mul_of_pos_left hbound hpos2
|
||||
_ = 3 := by field_simp [hs2pi_pos.ne.symm]
|
||||
exact ((lt_div_iff₀ hpos).mpr hineq)
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §4 INFINITE-LINE DENSITY
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
lemma peak_integrable_over_R (σ : ℝ) (hσ : σ > 0) (m : ℝ)
|
||||
(a b s t x₀ y₀ : ℝ) :
|
||||
Integrable (fun τ : ℝ =>
|
||||
gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) := by
|
||||
sorry
|
||||
|
||||
theorem ansatzLineDensity_decomp (σ : ℝ) (hσ : σ > 0)
|
||||
{k : ℕ} (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ)
|
||||
(hm : ∀ i, masses i ≥ 0) (a b s t : ℝ) :
|
||||
ansatzLineDensity σ positions masses a b s t =
|
||||
(Finset.univ : Finset (Fin k)).sum (fun i =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses i)
|
||||
(s + a * τ - (positions i).1, t + b * τ - (positions i).2)) := by
|
||||
unfold ansatzLineDensity gaussianAnsatz_eval
|
||||
rw [integral_finset_sum]
|
||||
intro i _
|
||||
exact (peak_integrable_over_R σ hσ (masses i) a b s t
|
||||
(positions i).1 (positions i).2)
|
||||
|
||||
theorem peak_contribution_nonneg
|
||||
(σ m x₀ y₀ s t a b : ℝ) (hσ : σ > 0) (hm : m ≥ 0) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) ≥ 0 := by
|
||||
apply integral_nonneg; intro τ; unfold gaussian2D; positivity
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §5 COLLINEARITY → UNIT DIRECTION
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem signedArea_zero_implies_perpDist_zero
|
||||
{k : ℕ} (positions : Fin k → ℝ × ℝ)
|
||||
{i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m)
|
||||
(halign : signedArea (positions i) (positions j) (positions m) = 0) :
|
||||
∃ (a b : ℝ), a ^ 2 + b ^ 2 = 1 ∧
|
||||
perpDistance (positions j).1 (positions j).2 a b
|
||||
(positions i).1 (positions i).2 = 0 ∧
|
||||
perpDistance (positions m).1 (positions m).2 a b
|
||||
(positions i).1 (positions i).2 = 0 := by
|
||||
sorry
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §6 COLLISION THEOREM — HORIZONTAL LINE CASE
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
lemma integrand_simp (x : ℝ) (τ : ℝ) : 0 + 1 * τ - x = τ - x := by ring
|
||||
lemma integrand_simp2 (y₀ : ℝ) : y₀ + 0 * τ - y₀ = 0 := by ring
|
||||
|
||||
theorem collinear_line_density_exceeds_two
|
||||
{σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit)
|
||||
{k : ℕ} (hk : k ≥ 3)
|
||||
(positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ)
|
||||
(hmass : ∀ i, masses i ≥ 1)
|
||||
(y₀ : ℝ)
|
||||
{i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m)
|
||||
(hi : (positions i).2 = y₀)
|
||||
(hj : (positions j).2 = y₀)
|
||||
(hm_pos : (positions m).2 = y₀) :
|
||||
ansatzLineDensity σ positions masses 1 0 0 y₀ > 2 := by
|
||||
let Λ := ansatzLineDensity σ positions masses 1 0 0 y₀
|
||||
have hmass_nn : ∀ l, masses l ≥ 0 :=
|
||||
fun l => le_trans (by norm_num : (0 : ℝ) ≤ 1) (hmass l)
|
||||
have hdecomp := ansatzLineDensity_decomp σ hσ positions masses hmass_nn 1 0 0 y₀
|
||||
have hnonneg : ∀ l : Fin k,
|
||||
(∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(0 + 1 * τ - (positions l).1, y₀ - (positions l).2)) ≥ 0 := by
|
||||
intro l
|
||||
have h := peak_contribution_nonneg σ (masses l) (positions l).1 (positions l).2
|
||||
0 y₀ 1 0 hσ (hmass_nn l)
|
||||
simpa using h
|
||||
have h_on_i :
|
||||
(∫ τ : ℝ, gaussian2D σ (masses i)
|
||||
(0 + 1 * τ - (positions i).1, y₀ - (positions i).2)) =
|
||||
masses i / (σ * Real.sqrt (2 * π)) := by
|
||||
calc
|
||||
(∫ τ : ℝ, gaussian2D σ (masses i) (0 + 1 * τ - (positions i).1, y₀ - (positions i).2))
|
||||
= (∫ τ : ℝ, gaussian2D σ (masses i) (τ - (positions i).1, 0)) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; simp [hi, integrand_simp]
|
||||
_ = masses i / (σ * Real.sqrt (2 * π)) :=
|
||||
on_line_contribution σ (masses i) (positions i).1 hσ (hmass_nn i)
|
||||
have h_on_j :
|
||||
(∫ τ : ℝ, gaussian2D σ (masses j)
|
||||
(0 + 1 * τ - (positions j).1, y₀ - (positions j).2)) =
|
||||
masses j / (σ * Real.sqrt (2 * π)) := by
|
||||
calc
|
||||
(∫ τ : ℝ, gaussian2D σ (masses j) (0 + 1 * τ - (positions j).1, y₀ - (positions j).2))
|
||||
= (∫ τ : ℝ, gaussian2D σ (masses j) (τ - (positions j).1, 0)) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; simp [hj, integrand_simp]
|
||||
_ = masses j / (σ * Real.sqrt (2 * π)) :=
|
||||
on_line_contribution σ (masses j) (positions j).1 hσ (hmass_nn j)
|
||||
have h_on_m :
|
||||
(∫ τ : ℝ, gaussian2D σ (masses m)
|
||||
(0 + 1 * τ - (positions m).1, y₀ - (positions m).2)) =
|
||||
masses m / (σ * Real.sqrt (2 * π)) := by
|
||||
calc
|
||||
(∫ τ : ℝ, gaussian2D σ (masses m) (0 + 1 * τ - (positions m).1, y₀ - (positions m).2))
|
||||
= (∫ τ : ℝ, gaussian2D σ (masses m) (τ - (positions m).1, 0)) := by
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; simp [hm_pos, integrand_simp]
|
||||
_ = masses m / (σ * Real.sqrt (2 * π)) :=
|
||||
on_line_contribution σ (masses m) (positions m).1 hσ (hmass_nn m)
|
||||
rw [hdecomp]
|
||||
have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity
|
||||
have hσs2pi_pos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos
|
||||
have hsum_ge_three :
|
||||
(Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2)) ≥
|
||||
3 / (σ * Real.sqrt (2 * π)) := by
|
||||
have hsubset : ({i, j, m} : Finset (Fin k)) ⊆ Finset.univ := Finset.subset_univ _
|
||||
have hnonneg_subset : ∀ l, (∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2)) ≥ 0 := by
|
||||
intro l; simpa using hnonneg l
|
||||
have hsubset_sum : (({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2))) ≤
|
||||
(Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2)) :=
|
||||
Finset.sum_le_sum_of_subset_of_nonneg hsubset (fun l _ _ => hnonneg_subset l)
|
||||
have h_conv_int : ∀ l, (positions l).2 = y₀ →
|
||||
(∫ τ : ℝ, gaussian2D σ (masses l) (1 * τ - (positions l).1, y₀ - (positions l).2)) =
|
||||
(∫ τ : ℝ, gaussian2D σ (masses l) (τ - (positions l).1, 0)) := by
|
||||
intro l hl
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; simp [hl, sub_self]
|
||||
have h3 : (({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2))) ≥
|
||||
3 / (σ * Real.sqrt (2 * π)) := by
|
||||
have hi_notin : i ∉ ({j, m} : Finset (Fin k)) := by
|
||||
intro hi
|
||||
have hi_mem_m : i ∈ ({m} : Finset (Fin k)) :=
|
||||
(Finset.mem_insert.mp hi).resolve_left hij
|
||||
exact him (Finset.mem_singleton.mp hi_mem_m)
|
||||
have hj_notin : j ∉ ({m} : Finset (Fin k)) := by
|
||||
intro hj; exact hjm (Finset.mem_singleton.mp hj)
|
||||
calc
|
||||
(({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
(1 * τ - (positions l).1, y₀ - (positions l).2)))
|
||||
= (({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l) (τ - (positions l).1, 0))) := by
|
||||
refine Finset.sum_congr rfl fun l hl => ?_
|
||||
have hl_out : l = i ∨ l = j ∨ l = m := by
|
||||
simpa [Finset.mem_insert, Finset.mem_singleton] using hl
|
||||
rcases hl_out with (hl_i|hl_j|hl_m)
|
||||
· rw [hl_i]; exact h_conv_int i hi
|
||||
· rw [hl_j]; exact h_conv_int j hj
|
||||
· rw [hl_m]; exact h_conv_int m hm_pos
|
||||
_ = (∫ τ : ℝ, gaussian2D σ (masses i) (τ - (positions i).1, 0)) +
|
||||
((∫ τ : ℝ, gaussian2D σ (masses j) (τ - (positions j).1, 0)) +
|
||||
(∫ τ : ℝ, gaussian2D σ (masses m) (τ - (positions m).1, 0))) := by
|
||||
rw [Finset.sum_insert hi_notin, Finset.sum_insert hj_notin, Finset.sum_singleton]
|
||||
_ = (masses i + masses j + masses m) / (σ * Real.sqrt (2 * π)) := by
|
||||
rw [on_line_contribution σ (masses i) (positions i).1 hσ (hmass_nn i),
|
||||
on_line_contribution σ (masses j) (positions j).1 hσ (hmass_nn j),
|
||||
on_line_contribution σ (masses m) (positions m).1 hσ (hmass_nn m)]
|
||||
field_simp [hσs2pi_pos.ne.symm]
|
||||
ring
|
||||
_ ≥ (1 + 1 + 1) / (σ * Real.sqrt (2 * π)) := by
|
||||
have hm_i : masses i ≥ 1 := hmass i
|
||||
have hm_j : masses j ≥ 1 := hmass j
|
||||
have hm_m : masses m ≥ 1 := hmass m
|
||||
refine (div_le_div_of_nonneg_right ?_ (le_of_lt hσs2pi_pos))
|
||||
linarith
|
||||
_ = 3 / (σ * Real.sqrt (2 * π)) := by norm_num
|
||||
linarith
|
||||
have hthree_gt_two := three_over_sroot2pi_gt_two hσ hσ_bound
|
||||
-- Now we need to relate the sum in the target to hsum_ge_three
|
||||
-- The target (after rw [hdecomp]) is:
|
||||
-- Σᵢ ∫ g2D(0+1*τ - ..., y₀+0*τ - ...) > 2
|
||||
-- But hsum_ge_three is about:
|
||||
-- Σᵢ ∫ g2D(1*τ - ..., y₀ - ...) ≥ 3/(σ√(2π))
|
||||
-- These sums are equal by integral_congr_ae.
|
||||
have h_sums_eq : (Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l) (0 + 1 * τ - (positions l).1, y₀ + 0 * τ - (positions l).2)) =
|
||||
(Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l) (1 * τ - (positions l).1, y₀ - (positions l).2)) := by
|
||||
refine Finset.sum_congr rfl fun l hl => ?_
|
||||
refine integral_congr_ae ?_
|
||||
filter_upwards with τ; simp
|
||||
rw [h_sums_eq]
|
||||
linarith
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §7 GENERAL LINE DIRECTION (sketch)
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem gaussian_line_integral_unit_dir
|
||||
(σ m a b s t x₀ y₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0)
|
||||
(hab : a ^ 2 + b ^ 2 = 1) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) =
|
||||
m / (σ * Real.sqrt (2 * π)) *
|
||||
Real.exp (-(perpDistance x₀ y₀ a b s t) ^ 2 / (2 * σ ^ 2)) := by
|
||||
sorry
|
||||
|
||||
theorem on_line_contribution_general
|
||||
(σ m a b s t x₀ y₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0)
|
||||
(hab : a ^ 2 + b ^ 2 = 1)
|
||||
(hon : perpDistance x₀ y₀ a b s t = 0) :
|
||||
(∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) =
|
||||
m / (σ * Real.sqrt (2 * π)) := by
|
||||
rw [gaussian_line_integral_unit_dir σ m a b s t x₀ y₀ hσ hm hab, hon]
|
||||
simp
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §8 COLLISION THEOREM — GENERAL DIRECTION
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem collinear_line_density_exceeds_two_general
|
||||
{σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit)
|
||||
{k : ℕ} (hk : k ≥ 3)
|
||||
(positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ)
|
||||
(hmass : ∀ i, masses i ≥ 1)
|
||||
{i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m)
|
||||
(halign : signedArea (positions i) (positions j) (positions m) = 0) :
|
||||
∃ (a b : ℝ) (_hab : a ^ 2 + b ^ 2 = 1),
|
||||
ansatzLineDensity σ positions masses a b
|
||||
(positions i).1 (positions i).2 > 2 := by
|
||||
obtain ⟨a, b, hab, hperp_j, hperp_m⟩ :=
|
||||
signedArea_zero_implies_perpDist_zero positions hij him hjm halign
|
||||
use a, b, hab
|
||||
have hmass_nn : ∀ l, masses l ≥ 0 :=
|
||||
fun l => le_trans (by norm_num : (0 : ℝ) ≤ 1) (hmass l)
|
||||
have hdecomp := ansatzLineDensity_decomp σ hσ positions masses hmass_nn
|
||||
a b (positions i).1 (positions i).2
|
||||
rw [hdecomp]
|
||||
have hnonneg : ∀ l : Fin k,
|
||||
(∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2)) ≥ 0 := by
|
||||
intro l; exact peak_contribution_nonneg σ (masses l) (positions l).1 (positions l).2
|
||||
(positions i).1 (positions i).2 a b hσ (hmass_nn l)
|
||||
have hperp_i : perpDistance (positions i).1 (positions i).2 a b
|
||||
(positions i).1 (positions i).2 = 0 := by
|
||||
unfold perpDistance; simp
|
||||
have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity
|
||||
have hσs2pi_pos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos
|
||||
have h3 : (({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2))) ≥
|
||||
3 / (σ * Real.sqrt (2 * π)) := by
|
||||
calc
|
||||
(({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2)))
|
||||
= (∫ τ : ℝ, gaussian2D σ (masses i)
|
||||
((positions i).1 + a * τ - (positions i).1,
|
||||
(positions i).2 + b * τ - (positions i).2)) +
|
||||
((∫ τ : ℝ, gaussian2D σ (masses j)
|
||||
((positions i).1 + a * τ - (positions j).1,
|
||||
(positions i).2 + b * τ - (positions j).2)) +
|
||||
(∫ τ : ℝ, gaussian2D σ (masses m)
|
||||
((positions i).1 + a * τ - (positions m).1,
|
||||
(positions i).2 + b * τ - (positions m).2))) := by
|
||||
simp [hij, him, hjm, Finset.sum_insert, Finset.sum_singleton]
|
||||
_ = (masses i / (σ * Real.sqrt (2 * π)) +
|
||||
masses j / (σ * Real.sqrt (2 * π)) +
|
||||
masses m / (σ * Real.sqrt (2 * π))) := by
|
||||
-- need on_line_contribution_general for i,j,m
|
||||
-- For i: positions (i) coincide, so perpDist = 0 by hperp_i
|
||||
-- For j: perpDist = 0 by hperp_j
|
||||
-- For m: perpDist = 0 by hperp_m
|
||||
sorry
|
||||
_ = (masses i + masses j + masses m) / (σ * Real.sqrt (2 * π)) := by ring
|
||||
_ ≥ (1 + 1 + 1) / (σ * Real.sqrt (2 * π)) := by
|
||||
have hm_i : masses i ≥ 1 := hmass i
|
||||
have hm_j : masses j ≥ 1 := hmass j
|
||||
have hm_m : masses m ≥ 1 := hmass m
|
||||
refine (div_le_div_of_nonneg_right ?_ (le_of_lt hσs2pi_pos))
|
||||
linarith
|
||||
_ = 3 / (σ * Real.sqrt (2 * π)) := by norm_num
|
||||
have hsum_ge_three : (Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2)) ≥
|
||||
3 / (σ * Real.sqrt (2 * π)) := by
|
||||
have hsubset_sum : (({i, j, m} : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2))) ≤
|
||||
(Finset.univ : Finset (Fin k)).sum (fun l =>
|
||||
∫ τ : ℝ, gaussian2D σ (masses l)
|
||||
((positions i).1 + a * τ - (positions l).1,
|
||||
(positions i).2 + b * τ - (positions l).2)) :=
|
||||
Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _) (fun l _ _ => hnonneg l)
|
||||
linarith
|
||||
have hthree := three_over_sroot2pi_gt_two hσ hσ_bound
|
||||
linarith
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §9 MAIN THEOREM
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
theorem no_collinear_at_zero_energy
|
||||
{σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit)
|
||||
{lam : ℝ} (hlam : lam > 0)
|
||||
{k : ℕ} (hk : k ≥ 3)
|
||||
(positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ)
|
||||
(hmass : ∀ i, masses i ≥ 1)
|
||||
{ι : Type*} [Fintype ι] [DecidableEq ι]
|
||||
(densities : ι → ℝ) (hE : energy lam densities = 0) :
|
||||
∀ i j m : Fin k, i ≠ j → i ≠ m → j ≠ m →
|
||||
signedArea (positions i) (positions j) (positions m) = 0 → False := by
|
||||
intro i j m hij him hjm halign
|
||||
sorry
|
||||
|
||||
end Semantics.N3L_Energy
|
||||
Loading…
Add table
Reference in a new issue