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

nsDuhamel_of_forall_kernelIntegral

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)

1285theorem nsDuhamel_of_forall_kernelIntegral {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1286    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1287    (hDC : ∀ t : ℝ, ∀ k : Mode2, DuhamelKernelDominatedConvergenceAt ν F_N F t k)
1288    (hId :
1289      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1290        (extendByZero (H.uN N t) k) =
1291          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1292            + (duhamelKernelIntegral ν (F_N N) t) k) :
1293    IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) HC.u := by

proof body

Tactic-mode proof.

1294  have hD :
1295      ∀ t : ℝ, ∀ k : Mode2,
1296        Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
1297          (nhds (((duhamelKernelIntegral ν F) t) k)) := by
1298    intro t k
1299    exact tendsto_duhamelKernelIntegral_of_dominated_convergence (ν := ν) (F_N := F_N) (F := F) (t := t) (k := k)
1300      (hDC t k)
1301  exact
1302    nsDuhamel_of_forall (HC := HC) (ν := ν)
1303      (D_N := fun N => duhamelKernelIntegral ν (F_N N)) (D := duhamelKernelIntegral ν F)
1304      (hD := hD) (hId := hId)
1305
1306/-- Variant of `nsDuhamel_of_forall_kernelIntegral` that assumes dominated convergence only for the
1307*forcing* (not the kernel integrand), plus `0 ≤ ν` and `t ≥ 0` to control the kernel factor. -/

used by (2)

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

depends on (26)

Lean names referenced from this declaration's body.