duhamelKernelIntegral

formal source

 652/-- The Duhamel kernel operator applied to a (Fourier-modewise) forcing trajectory:
 653
 654`(duhamelKernelIntegral ν F)(t,k) = -∫₀ᵗ heatFactor ν (t-s) k • F(s,k) ds`. -/
 655noncomputable def duhamelKernelIntegral (ν : ℝ) (F : ℝ → FourierState2D) : ℝ → FourierState2D :=
 656  fun t k => -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (F s k)
 657
 658/-- Hypothesis (at fixed `t,k`): the Duhamel-kernel integrands satisfy the assumptions of dominated
 659convergence, so the corresponding interval integrals converge. -/
 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,