From 15225feff704743929c608861e9f15a203fea2dd Mon Sep 17 00:00:00 2001 From: allaun Date: Wed, 17 Jun 2026 05:10:49 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20add=20DiscreteContinuousBound=20?= =?UTF-8?q?=E2=80=94=20exponential=20error=20bound=20via=20Gronwall?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Defines coupling matrix A = (ε/2)·[[0,1],[1,0]], proves ‖A‖ = |ε|/2, and applies Mathlib Gronwall for the discrete-continuous coupling bound: ‖e(t)‖ ≤ ‖e(0)‖ · exp(|ε|/2 · (t-a)) Includes trajectory distance variants (interval + global). --- .../Semantics/DiscreteContinuousBound.lean | 209 ++++++++++++++++++ 1 file changed, 209 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/DiscreteContinuousBound.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics/DiscreteContinuousBound.lean b/0-Core-Formalism/lean/Semantics/Semantics/DiscreteContinuousBound.lean new file mode 100644 index 00000000..1060fbbd --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/DiscreteContinuousBound.lean @@ -0,0 +1,209 @@ +import Mathlib.Analysis.ODE.Gronwall +import Mathlib.Analysis.Matrix.Normed +import Mathlib.Analysis.SpecialFunctions.ExpDeriv + +/-! +# DiscreteContinuousBound.lean + +Exponential error bound for discrete–continuous coupling via Grönwall's inequality. + +Given the 2×2 coupling matrix A = (ε/2) · [[0,1],[1,0]], +we prove: + 1. ‖A‖ = |ε|/2 (operator norm) + 2. ‖e(t)‖ ≤ ‖e(0)‖ · exp(|ε|/2 · t) (Grönwall bound on coupling error) + +The proof uses Mathlib's `norm_le_gronwallBound_of_norm_deriv_right_le` +and the ∞-operator-norm on matrices (`linfty_opNorm`). +-/ + +open Matrix Set Filter Real +open scoped Topology + +namespace Semantics.DiscreteContinuousBound + +variable {ε : ℝ} + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §1 The 2×2 Coupling Matrix +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- The off-diagonal exchange matrix M₀ = [[0,1],[1,0]]. -/ +def M₀ : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; 1, 0] + +/-- The coupling matrix A = (ε/2) · M₀ = (ε/2) · [[0,1],[1,0]]. -/ +def A (ε : ℝ) : Matrix (Fin 2) (Fin 2) ℝ := (ε / 2) • M₀ + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §2 Operator Norm: ‖A‖ = |ε|/2 +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- Entry (0,1) of the coupling matrix is ε/2. -/ +@[simp] lemma A_apply_zero_one : A ε 0 1 = ε / 2 := by + simp [A, M₀, smul_apply] + +/-- Entry (1,0) of the coupling matrix is ε/2. -/ +@[simp] lemma A_apply_one_zero : A ε 1 0 = ε / 2 := by + simp [A, M₀, smul_apply] + +/-- Entry (0,0) of the coupling matrix is 0. -/ +@[simp] lemma A_apply_zero_zero : A ε 0 0 = 0 := by + simp [A, M₀, smul_apply] + +/-- Entry (1,1) of the coupling matrix is 0. -/ +@[simp] lemma A_apply_one_one : A ε 1 1 = 0 := by + simp [A, M₀, smul_apply] + +/-- All entries of A satisfy ‖A i j‖ ≤ |ε/2|. -/ +lemma A_entry_bound (i j : Fin 2) : ‖A ε i j‖ ≤ |ε / 2| := by + fin_cases i <;> fin_cases j <;> simp [abs_nonneg] + +/-- The ∞-operator norm of A equals |ε|/2. + + Strategy: antisymmetry. + • Upper bound: every entry ≤ |ε/2|, so sup ≤ |ε/2| via `norm_le_iff`. + • Lower bound: entry (0,1) = ε/2, so ‖A‖ ≥ |ε/2| via `norm_entry_le_entrywise_sup_norm`. +-/ +theorem coupling_opNorm (ε : ℝ) : ‖A ε‖ = |ε| / 2 := by + have hε2 : |ε / 2| = |ε| / 2 := by rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)] + -- Upper bound: ‖A‖ ≤ |ε/2| + have h_upper : ‖A ε‖ ≤ |ε / 2| := by + rw [norm_le_iff (abs_nonneg _)] + exact A_entry_bound + -- Lower bound: |ε/2| ≤ ‖A‖ (witness: entry (0,1)) + have h_lower : |ε / 2| ≤ ‖A ε‖ := by + have : ‖A ε 0 1‖ ≤ ‖A ε‖ := norm_entry_le_entrywise_sup_norm _ + simp_all + -- Combine + linarith [h_upper, h_lower] + +/-- Variant: ‖A‖₊ = |ε|/2 as NNReals. -/ +theorem coupling_opNNNorm (ε : ℝ) : ‖A ε‖₊ = Real.toNNReal (|ε| / 2) := by + ext; exact coupling_opNorm ε + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §3 Lipschitz Constant of the Linear Flow x ↦ A·x +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- The linear map v ↦ A *ᵥ v is Lipschitz with constant ‖A‖₊ = |ε|/2. + + This follows from the ∞-operator-norm submultiplicativity: + ‖A *ᵥ v‖ ≤ ‖A‖ · ‖v‖ + Combined with `ContinuousLinearMap.lipschitzWith_opNorm` or a direct proof. +-/ +theorem coupling_lipschitzWith (ε : ℝ) : + LipschitzWith (Real.toNNReal (|ε| / 2)) (fun v : Fin 2 → ℝ => A ε *ᵥ v) := by + -- Step 1: LipschitzWith ‖mulVecLin (A ε)‖₊ + have h_lip : LipschitzWith ‖mulVecLin (A ε)‖₊ (fun v => A ε *ᵥ v) := + (mulVecLin (A ε)).lipschitz + -- Step 2: ‖mulVecLin (A ε)‖₊ = ‖A ε‖₊ (linfty_opNNNorm_eq_opNNNorm) + have h_norm : ‖mulVecLin (A ε)‖₊ = ‖A ε‖₊ := by + rw [← linfty_opNNNorm_eq_opNNNorm] + -- Step 3: ‖A ε‖₊ = Real.toNNReal (|ε|/2) + rw [coupling_opNNNorm] at h_norm + rwa [h_norm] at h_lip + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §4 Grönwall Exponential Error Bound +-- ═══════════════════════════════════════════════════════════════════════════════ + +section GronwallBound + +variable {a b : ℝ} + +/-- **Discrete–Continuous Coupling Bound (Grönwall form).** + +If `e : ℝ → Fin 2 → ℝ` satisfies the linear ODE e' = A · e on `[a, b]`, +and the initial error is bounded by δ, then: + + ‖e(t)‖ ≤ δ · exp(|ε|/2 · (t - a)) for all t ∈ [a, b]. + +This is a direct application of `norm_le_gronwallBound_of_norm_deriv_right_le` +with K = |ε|/2 and ε_g = 0 (exact ODE, no perturbation). +-/ +theorem norm_le_gronwallBound_of_coupling + {e e' : ℝ → Fin 2 → ℝ} {δ : ℝ} (hδ : 0 ≤ δ) + (he_cont : ContinuousOn e (Icc a b)) + (he_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt e (e' t) (Ici t) t) + (he_ode : ∀ t ∈ Ico a b, e' t = A ε *ᵥ e t) + (he_init : ‖e a‖ ≤ δ) : + ∀ t ∈ Icc a b, ‖e t‖ ≤ gronwallBound δ (|ε| / 2) 0 (t - a) := by + apply norm_le_gronwallBound_of_norm_deriv_right_le he_cont he_deriv he_init + intro t ht + -- Goal: ‖e' t‖ ≤ (|ε|/2) · ‖e t‖ + 0 + rw [he_ode t ht, add_zero] + -- Goal: ‖A ε *ᵥ e t‖ ≤ (|ε|/2) · ‖e t‖ + have := linfty_opNorm_mulVec (A ε) (e t) + rw [coupling_opNorm] at this + exact this + +/-- **Clean exponential form** (using `gronwallBound_ε0`). + +When the ODE is exact (ε_g = 0), the Grönwall bound simplifies to: + ‖e(t)‖ ≤ ‖e(0)‖ · exp(|ε|/2 · (t - a)) +-/ +theorem discrete_continuous_bound + {e e' : ℝ → Fin 2 → ℝ} {δ : ℝ} (hδ : 0 ≤ δ) + (he_cont : ContinuousOn e (Icc a b)) + (he_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt e (e' t) (Ici t) t) + (he_ode : ∀ t ∈ Ico a b, e' t = A ε *ᵥ e t) + (he_init : ‖e a‖ ≤ δ) : + ∀ t ∈ Icc a b, ‖e t‖ ≤ δ * exp (|ε| / 2 * (t - a)) := by + intro t ht + have h := norm_le_gronwallBound_of_coupling hδ he_cont he_deriv he_ode he_init t ht + rwa [gronwallBound_ε0] at h + +/-- **ODE-trajectory version** via Mathlib's `dist_le_of_trajectories_ODE`. + +If `f` and `g` are two trajectories of the linear ODE ẋ = A · x on `[a, b]`, +then their distance grows at most exponentially: + dist(f(t), g(t)) ≤ dist(f(a), g(a)) · exp(|ε|/2 · (t - a)) +-/ +theorem trajectory_dist_bound + {f g : ℝ → Fin 2 → ℝ} + (hf_cont : ContinuousOn f (Icc a b)) + (hf_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt f (A ε *ᵥ f t) (Ici t) t) + (hg_cont : ContinuousOn g (Icc a b)) + (hg_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt g (A ε *ᵥ g t) (Ici t) t) + {δ : ℝ} (hδ : 0 ≤ δ) (h_init : dist (f a) (g a) ≤ δ) : + ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (|ε| / 2 * (t - a)) := by + intro t ht + -- Apply `dist_le_of_trajectories_ODE` with K = |ε|/2 + have hv : ∀ t, LipschitzWith (Real.toNNReal (|ε| / 2)) (fun x => A ε *ᵥ x) := + fun _ => coupling_lipschitzWith ε + have h := dist_le_of_trajectories_ODE hv hf_cont hf_deriv hg_cont hg_deriv h_init t ht + -- Rewrite: the K in `dist_le_of_trajectories_ODE` is a `ℝ≥0`, and + -- it appears as (K : ℝ) * (t - a) in the exponent. + -- After the LipschitzWith substitution we need: ↑(Real.toNNReal (|ε|/2)) = |ε|/2 + have hnn : |ε| / 2 ≥ 0 := div_nonneg (abs_nonneg _) (by norm_num) + rw [Real.coe_toNNReal _ hnn] at h + exact h + +/-- **Global version**: on all of ℝ, two trajectories of ẋ = A · x satisfy + dist(f(t), g(t)) ≤ dist(f(a), g(a)) · exp(|ε|/2 · |t - a|) +-/ +theorem trajectory_dist_bound_univ + {f g : ℝ → Fin 2 → ℝ} + (hf : ∀ t, HasDerivAt f (A ε *ᵥ f t) t) + (hg : ∀ t, HasDerivAt g (A ε *ᵥ g t) t) + (a t : ℝ) : + dist (f t) (g t) ≤ dist (f a) (g a) * exp (|ε| / 2 * |t - a|) := by + wlog hle : a ≤ t with h + -- t < a: swap and use symmetry + have := h hg hf t a (le_of_not_le hle) + rw [dist_comm (f t) (g t), dist_comm (f a) (g a), abs_sub_comm] at this + exact this + -- a ≤ t: use the interval version on [a, t] + have hnn : |ε| / 2 ≥ 0 := div_nonneg (abs_nonneg _) (by norm_num) + have hlip : ∀ s, LipschitzWith (Real.toNNReal (|ε| / 2)) (fun x => A ε *ᵥ x) := + fun _ => coupling_lipschitzWith ε + have h := + dist_le_of_trajectories_ODE hlip + (hf.continuousOn) (fun s _ => (hf s).hasDerivWithinAt) + (hg.continuousOn) (fun s _ => (hg s).hasDerivWithinAt) + le_rfl t ⟨hle, le_rfl⟩ + rw [Real.coe_toNNReal _ hnn, sub_nonneg.mpr hle, abs_of_nonneg (sub_nonneg.mpr hle)] at h + exact h + +end GronwallBound + +end Semantics.DiscreteContinuousBound