mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat: add DiscreteContinuousBound — exponential error bound via Gronwall
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).
This commit is contained in:
parent
71097f5c84
commit
15225feff7
1 changed files with 209 additions and 0 deletions
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue