pith. machine review for the scientific record. sign in
theorem proved tactic proof

nsDuhamel_of_forall_kernelIntegral_of_forcing

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

1308theorem nsDuhamel_of_forall_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1309    (ν : ℝ) (hν : 0 ≤ ν)
1310    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1311    (hF :
1312      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)

proof body

Tactic-mode proof.

1313    (hId :
1314      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1315        (extendByZero (H.uN N t) k) =
1316          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1317            + (duhamelKernelIntegral ν (F_N N) t) k) :
1318    IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) HC.u := by
1319  intro t ht k
1320  -- convergence of the main trajectory at time `t` and at time `0`
1321  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1322    HC.converges t k
1323  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1324    HC.converges 0 k
1325  -- convergence of the kernel-integral remainder at time `t` (from forcing-level DCT)
1326  have hconv_D :
1327      Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
1328        (nhds (((duhamelKernelIntegral ν F) t) k)) := by
1329    have hDC : DuhamelKernelDominatedConvergenceAt ν F_N F t k :=
1330      duhamelKernelDominatedConvergenceAt_of_forcing (ν := ν) (t := t) hν ht (hF t ht k)
1331    exact
1332      tendsto_duhamelKernelIntegral_of_dominated_convergence (ν := ν) (F_N := F_N) (F := F) (t := t) (k := k)
1333        hDC
1334  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1335  have hsmul :
1336      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1337        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1338    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1339    exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1340  -- combine the smul part and the remainder part
1341  have hsum :
1342      Tendsto (fun N : ℕ =>
1343        (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (duhamelKernelIntegral ν (F_N N) t) k) atTop
1344          (nhds ((heatFactor ν t k) • ((HC.u 0) k) + ((duhamelKernelIntegral ν F) t) k)) :=
1345    hsmul.add hconv_D
1346  -- the identity holds for every N, hence the two sequences are eventually equal
1347  have hEq :
1348      (fun N : ℕ => extendByZero (H.uN N t) k)
1349        =ᶠ[atTop]
1350          (fun N : ℕ =>
1351            (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (duhamelKernelIntegral ν (F_N N) t) k) := by
1352    refine Filter.Eventually.of_forall ?_
1353    intro N
1354    exact hId N t ht k
1355  -- uniqueness of limits in a T2 space
1356  have :
1357      (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) + ((duhamelKernelIntegral ν F) t) k :=
1358    tendsto_nhds_unique_of_eventuallyEq hconv_t hsum hEq
1359  simpa [IsNSDuhamelTraj] using this
1360
1361end ConvergenceHypothesis
1362
1363/-- Convenience constructor: if each coefficient sequence is *eventually equal* to the corresponding
1364limit coefficient, then it tends to that limit. -/
1365noncomputable def ConvergenceHypothesis.ofEventuallyEq
1366    (H : UniformBoundsHypothesis)
1367    (u : ℝ → FourierState2D)
1368    (heq :
1369      ∀ t : ℝ, ∀ k : Mode2,
1370        (fun N : ℕ => (extendByZero (H.uN N t)) k) =ᶠ[atTop] (fun _ : ℕ => (u t) k)) :
1371    ConvergenceHypothesis H :=
1372  { u := u
1373    converges := by
1374      intro t k
1375      have hconst : Tendsto (fun _ : ℕ => (u t) k) atTop (𝓝 ((u t) k)) :=
1376        tendsto_const_nhds
1377      exact (tendsto_congr' (heq t k)).2 hconst }
1378
1379/-- Hypothesis: the limit object satisfies the intended PDE identity (kept abstract here). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more