duhamelKernelDominatedConvergenceAt_of_forcing

formal source

 743      exact MeasureTheory.ae_of_all _ (fun s hs => h_lim s hs) }
 744
 745/-- Convert a forcing-level dominated convergence hypothesis into the kernel-level one. -/
 746noncomputable def duhamelKernelDominatedConvergenceAt_of_forcing
 747    {ν t : ℝ} (hν : 0 ≤ ν) (ht : 0 ≤ t)
 748    {F_N : ℕ → ℝ → FourierState2D} {F : ℝ → FourierState2D} {k : Mode2}
 749    (hF : ForcingDominatedConvergenceAt F_N F t k) :
 750    DuhamelKernelDominatedConvergenceAt ν F_N F t k := by
 751  classical
 752  refine
 753    { bound := hF.bound
 754      h_meas := ?_
 755      h_bound := ?_
 756      bound_integrable := hF.bound_integrable
 757      h_lim := ?_ }
 758  · -- measurability: `heatFactor( t - s )` is continuous, and `smul` preserves AE-strong measurability
 759    have hheat_meas :
 760        MeasureTheory.AEStronglyMeasurable (fun s : ℝ => heatFactor ν (t - s) k)
 761          (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)) := by
 762      -- continuity in `s`
 763      have hcont : Continuous fun s : ℝ => heatFactor ν (t - s) k := by
 764        -- unfold the scalar kernel and use continuity of `Real.exp`
 765        -- `s ↦ exp (-ν * kSq k * (t - s))`
 766        have hlin : Continuous fun s : ℝ => (-ν * kSq k) * (t - s) := by
 767          exact (continuous_const.mul (continuous_const.sub continuous_id))
 768        simpa [heatFactor, mul_assoc] using (continuous_exp.comp hlin)
 769      exact hcont.aestronglyMeasurable
 770    refine hF.h_meas.mono ?_
 771    intro N hmeasN
 772    exact hheat_meas.smul hmeasN
 773  · -- domination: `|heatFactor| ≤ 1` on `s ∈ uIoc 0 t` (for `t ≥ 0`, `ν ≥ 0`)
 774    refine hF.h_bound.mono ?_
 775    intro N hboundN
 776    filter_upwards [hboundN] with s hsBound