latticeSpacing_tendsto_zero

formal source

  59  div_pos hL (Nat.cast_pos.mpr hN)
  60
  61/-- The lattice spacing vanishes in the continuum limit: L/N → 0 as N → ∞. -/
  62theorem latticeSpacing_tendsto_zero (L : ℝ) (_hL : 0 < L) :
  63    ∀ ε > 0, ∃ N₀ : ℕ, 0 < N₀ ∧ ∀ N : ℕ, N₀ ≤ N → latticeSpacing L N < ε := by
  64  intro ε hε
  65  obtain ⟨N₀, hN₀⟩ := exists_nat_gt (L / ε)
  66  refine ⟨N₀ + 1, Nat.succ_pos _, fun N hN => ?_⟩
  67  unfold latticeSpacing
  68  have hN_pos : (0 : ℝ) < (N : ℝ) := Nat.cast_pos.mpr (by omega)
  69  rw [div_lt_iff₀ hN_pos]
  70  have hN₀_le : (N₀ : ℝ) ≤ (N : ℝ) := Nat.cast_le.mpr (by omega)
  71  nlinarith [div_lt_iff₀ hε |>.mp hN₀]
  72
  73/-! ## §2 Flat Spacetime Chain -/
  74
  75/-- The flat-spacetime chain: from J-cost through Minkowski to vanishing Einstein.
  76
  77    J(1+ε) = ε²/2 + O(ε⁴)  →  spatial metric g_ij = δ_ij  →
  78    η = diag(-1,+1,+1,+1)  →  Γ = 0  →  R^ρ_σμν = 0  →
  79    R_μν = 0  →  R = 0  →  G_μν = 0 -/
  80structure FlatChain : Prop where
  81  minkowski_christoffel : ∀ x ρ μ ν,
  82    christoffel minkowski_tensor x ρ μ ν = 0
  83  minkowski_riemann : ∀ x up low,
  84    riemann_tensor minkowski_tensor x up low = 0
  85  minkowski_ricci : ∀ x up low,
  86    ricci_tensor minkowski_tensor x up low = 0
  87  minkowski_scalar : ∀ x,
  88    ricci_scalar minkowski_tensor x = 0
  89  minkowski_einstein : ∀ x up low,
  90    einstein_tensor minkowski_tensor x up low = 0
  91
  92/-- The flat chain holds. All fields proved in `Curvature.lean`. -/