pith. machine review for the scientific record. sign in
structure definition def or abbrev

DuhamelKernelDominatedConvergenceAt

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)

 660structure DuhamelKernelDominatedConvergenceAt
 661    (ν : ℝ) (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
 662    (t : ℝ) (k : Mode2) where
 663  /-- An `L¹` bound for the integrands on `0..t`. -/
 664  bound : ℝ → ℝ
 665  /-- Strong measurability (eventually in `N`) on the relevant interval. -/
 666  h_meas :
 667    ∀ᶠ N : ℕ in atTop,
 668      MeasureTheory.AEStronglyMeasurable
 669        (fun s : ℝ => (heatFactor ν (t - s) k) • (F_N N s k))
 670        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 671  /-- Dominating bound (eventually in `N`) on the relevant interval. -/
 672  h_bound :
 673    ∀ᶠ N : ℕ in atTop,
 674      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 675        ‖(heatFactor ν (t - s) k) • (F_N N s k)‖ ≤ bound s
 676  /-- Integrability of the bound. -/
 677  bound_integrable :
 678    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 679  /-- Pointwise (ae on the interval) convergence of the integrands. -/
 680  h_lim :
 681    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 682      Tendsto (fun N : ℕ => (heatFactor ν (t - s) k) • (F_N N s k)) atTop
 683        (𝓝 ((heatFactor ν (t - s) k) • (F s k)))
 684
 685/-- A more user-facing dominated-convergence hypothesis at fixed `t,k` for the *forcing* itself,
 686without baking in the Duhamel kernel factor. Under `0 ≤ ν` and `0 ≤ t`, this implies
 687`DuhamelKernelDominatedConvergenceAt` because `|heatFactor ν (t-s) k| ≤ 1` on `s ∈ Set.uIoc 0 t`. -/

used by (8)

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

depends on (21)

Lean names referenced from this declaration's body.