From 7fa54f19b82d9478f1f4aa2f5c0f98b9fa48c822 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 11 Nov 2026 06:06:52 +0000 Subject: [PATCH] =?UTF-8?q?Br=C3=A4nd=C3=A9n=E2=80=93Leite:=20use=20r=20?= =?UTF-8?q?=E2=89=A0=200=20instead=20of=200=20<=20r=20for=20natural-number?= =?UTF-8?q?=20hypotheses?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Project style prefers n ≠ 0 over positivity for ℕ. Leftover from the 11-08 review of the Codex-written Brändén–Leite files (#2442); no downstream users. Co-Authored-By: Claude Opus 5.5 --- RealRooted/BrandenLeite/MarkedShift.lean | 4 ++-- .../BrandenLeite/OptionalRiseMatrix.lean | 6 +++--- .../BrandenLeite/WeightedShiftTiling.lean | 20 +++++++++---------- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/RealRooted/BrandenLeite/MarkedShift.lean b/RealRooted/BrandenLeite/MarkedShift.lean index 9288a3a5e..88922e5c5 100644 --- a/RealRooted/BrandenLeite/MarkedShift.lean +++ b/RealRooted/BrandenLeite/MarkedShift.lean @@ -141,7 +141,7 @@ theorem markedShiftKernel_apply_eq_zero_of_lt_add /-- Positive mark order makes the limiting marked kernel strictly lower. -/ theorem markedShiftKernel_apply_eq_zero_of_le - (as : List (ℕ → ℝ)) (N : ℕ) {r : ℕ} (hr : 0 < r) + (as : List (ℕ → ℝ)) (N : ℕ) {r : ℕ} (hr : r ≠ 0) {i j : Fin (N + 1)} (h : i.val ≤ j.val) : markedShiftKernel as N r i j = 0 := markedShiftKernel_apply_eq_zero_of_lt_add as N r (by lia) @@ -248,7 +248,7 @@ rows are in zero-aware interlacing. -/ theorem weightedGreenKernel_markedShiftKernel_pf_and_interl {b : ℕ → ℝ} (hb : ∀ n, 0 ≤ b n) {as : List (ℕ → ℝ)} (has : ∀ a ∈ as, ∀ n, 0 ≤ a n) - (N : ℕ) {r : ℕ} (hr : 0 < r) : + (N : ℕ) {r : ℕ} (hr : r ≠ 0) : (∀ i, IsPFPolynomial (kernelRow (weightedGreenKernel b N) (markedShiftKernel as N r) i)) ∧ ∀ i : Fin N, diff --git a/RealRooted/BrandenLeite/OptionalRiseMatrix.lean b/RealRooted/BrandenLeite/OptionalRiseMatrix.lean index d156b0260..59bb8927f 100644 --- a/RealRooted/BrandenLeite/OptionalRiseMatrix.lean +++ b/RealRooted/BrandenLeite/OptionalRiseMatrix.lean @@ -178,14 +178,14 @@ theorem orderedOptionalRiseCoefficient_eq_zero_of_lt /-- Positive-lag coefficients vanish when every optional-rise weight is zero. -/ theorem orderedOptionalRiseCoefficient_eq_zero_of_weights (as : List (ℕ → ℝ)) - (has : ∀ a ∈ as, ∀ n, a n = 0) {n j : ℕ} (hj : 0 < j) : + (has : ∀ a ∈ as, ∀ n, a n = 0) {n j : ℕ} (hj : j ≠ 0) : orderedOptionalRiseCoefficient as n j = 0 := by induction as generalizing n j with | nil => - obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj.ne' + obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj rfl | cons a as ih => - obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj.ne' + obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj rw [orderedOptionalRiseCoefficient, ih (fun b hb m => has b (by simp [hb]) m) (by simp), has a (by simp) n] diff --git a/RealRooted/BrandenLeite/WeightedShiftTiling.lean b/RealRooted/BrandenLeite/WeightedShiftTiling.lean index e2612f875..42b159a88 100644 --- a/RealRooted/BrandenLeite/WeightedShiftTiling.lean +++ b/RealRooted/BrandenLeite/WeightedShiftTiling.lean @@ -102,7 +102,7 @@ def weightedShiftTilingRow theorem weightedShiftTilingRow_isPFPolynomial {b : ℕ → ℝ} (hb : ∀ n, 0 ≤ b n) {as : List (ℕ → ℝ)} (has : ∀ a ∈ as, ∀ n, 0 ≤ a n) - (N : ℕ) {r : ℕ} (hr : 0 < r) (i : Fin (N + 1)) : + (N : ℕ) {r : ℕ} (hr : r ≠ 0) (i : Fin (N + 1)) : IsPFPolynomial (weightedShiftTilingRow b as N r i) := (weightedGreenKernel_markedShiftKernel_pf_and_interl hb has N hr).1 i @@ -111,7 +111,7 @@ theorem weightedShiftTilingRow_isPFPolynomial theorem interl_weightedShiftTilingRow_succ {b : ℕ → ℝ} (hb : ∀ n, 0 ≤ b n) {as : List (ℕ → ℝ)} (has : ∀ a ∈ as, ∀ n, 0 ≤ a n) - (N : ℕ) {r : ℕ} (hr : 0 < r) (i : Fin N) : + (N : ℕ) {r : ℕ} (hr : r ≠ 0) (i : Fin N) : Interl (weightedShiftTilingRow b as N r i.castSucc) (weightedShiftTilingRow b as N r i.succ) := (weightedGreenKernel_markedShiftKernel_pf_and_interl @@ -140,7 +140,7 @@ theorem coeff_zero_weightedShiftTilingRow_pos row recurrence. -/ theorem weightedShiftTilingRow_eq_global (b : ℕ → ℝ) (as : List (ℕ → ℝ)) (N : ℕ) - {r : ℕ} (hr : 0 < r) (i : Fin (N + 1)) : + {r : ℕ} (hr : r ≠ 0) (i : Fin (N + 1)) : weightedShiftTilingRow b as N r i = C (weightedGreenKernel b N i 0) + X * ∑ j : Fin (N + 1), @@ -180,7 +180,7 @@ theorem weightedShiftTilingRow_eq_global vector recurrence. -/ theorem weightedShiftTilingRow_succ_eq (b : ℕ → ℝ) (as : List (ℕ → ℝ)) {N : ℕ} - (s : Fin N) {r : ℕ} (hr : 0 < r) : + (s : Fin N) {r : ℕ} (hr : r ≠ 0) : weightedShiftTilingRow b as N r s.succ = C (b (s.val + 1)) * weightedShiftTilingRow b as N r s.castSucc + X * ∑ j : Fin (N + 1), @@ -207,7 +207,7 @@ theorem weightedShiftTilingRow_succ_eq ordered strict-selection coefficients. -/ theorem weightedShiftTilingRow_succ_eq_orderedOptionalRiseCoefficient (b : ℕ → ℝ) (as : List (ℕ → ℝ)) {N : ℕ} - (s : Fin N) {r : ℕ} (hr : 0 < r) : + (s : Fin N) {r : ℕ} (hr : r ≠ 0) : weightedShiftTilingRow b as N r s.succ = C (b (s.val + 1)) * weightedShiftTilingRow b as N r s.castSucc + X * ∑ j : Fin (N + 1), @@ -323,7 +323,7 @@ theorem orderedOptionalRiseCoefficient_map_mul `a * w n`. -/ theorem weightedShiftTilingRow_succ_eq_separated (b : ℕ → ℝ) (alphas : List ℝ) (w : ℕ → ℝ) {N : ℕ} - (s : Fin N) {r : ℕ} (hr : 0 < r) : + (s : Fin N) {r : ℕ} (hr : r ≠ 0) : weightedShiftTilingRow b (alphas.map fun a n => a * w n) N r s.succ = C (b (s.val + 1)) * weightedShiftTilingRow b (alphas.map fun a n => a * w n) @@ -353,7 +353,7 @@ theorem weightedShiftTilingRow_separated_isPFPolynomial {b : ℕ → ℝ} (hb : ∀ n, 0 ≤ b n) {alphas : List ℝ} (halphas : ∀ a ∈ alphas, 0 ≤ a) {w : ℕ → ℝ} (hw : ∀ n, 0 ≤ w n) - (N : ℕ) {r : ℕ} (hr : 0 < r) (i : Fin (N + 1)) : + (N : ℕ) {r : ℕ} (hr : r ≠ 0) (i : Fin (N + 1)) : IsPFPolynomial (weightedShiftTilingRow b (alphas.map fun a n => a * w n) N r i) := by refine weightedShiftTilingRow_isPFPolynomial hb ?_ N hr i @@ -419,7 +419,7 @@ theorem markedShiftKernel_eq_lowerShift_pow_of_weights_eq_zero by_cases hji : j.val ≤ i.val · rw [ite_eq_left hji, orderedOptionalRiseCoefficient_eq_zero_of_weights as has - (show 0 < i.val - j.val by lia)] + (show i.val - j.val ≠ 0 by lia)] simp [hij] · simp [hji, hij] rw [markedShiftKernel, hoptional, Matrix.one_mul] @@ -492,7 +492,7 @@ theorem sum_markedShiftKernel_pair /-- Exact three-term marked part of the two-factor nonstationary recurrence. -/ theorem weightedShiftTilingRow_pair_succ_eq (b u v : ℕ → ℝ) {N : ℕ} (s : Fin N) {r : ℕ} - (hr : 0 < r) (hri : r + 2 ≤ s.succ.val) : + (hr : r ≠ 0) (hri : r + 2 ≤ s.succ.val) : weightedShiftTilingRow b [u, v] N r s.succ = C (b (s.val + 1)) * weightedShiftTilingRow b [u, v] N r s.castSucc + X * (weightedShiftTilingRow b [u, v] N r @@ -520,7 +520,7 @@ theorem coeff_zero_weightedShiftTilingRow_eq_prod_range @[simp] theorem weightedShiftTilingRow_zero (b : ℕ → ℝ) (as : List (ℕ → ℝ)) (N : ℕ) - {r : ℕ} (hr : 0 < r) : + {r : ℕ} (hr : r ≠ 0) : weightedShiftTilingRow b as N r 0 = 1 := by have hdegree : (weightedShiftTilingRow b as N r 0).natDegree ≤ 0 := natDegree_kernelRow_le_row (weightedGreenKernel b N)