forcingDCTAt

formal source

1005
1006/-- Build `ForcingDominatedConvergenceAt` for the Galerkin forcing from the more concrete hypothesis
1007`GalerkinForcingDominatedConvergenceHypothesis`. -/
1008noncomputable def forcingDCTAt
1009    {H : UniformBoundsHypothesis} {Bop : (N : ℕ) → ConvectionOp N}
1010    (hF : GalerkinForcingDominatedConvergenceHypothesis H Bop)
1011    (t : ℝ) (ht : 0 ≤ t) (k : Mode2) :
1012    ForcingDominatedConvergenceAt (F_N := galerkinForcing H Bop) (F := hF.F) t k :=
1013  ForcingDominatedConvergenceAt.of_forall (F_N := galerkinForcing H Bop) (F := hF.F) (t := t) (k := k)
1014    (bound := hF.bound t k)
1015    (h_meas := by intro N; exact hF.meas N t ht k)
1016    (h_bound := by intro N s hs; exact hF.dom N t ht k s hs)
1017    (bound_integrable := hF.bound_integrable t ht k)
1018    (h_lim := by intro s hs; exact hF.lim t ht k s hs)
1019
1020/-- If each Galerkin trajectory `uN N` is continuous and each `Bop N` is continuous as a map
1021`(u,v) ↦ Bop N u v`, then each forcing mode `s ↦ (galerkinForcing H Bop N s) k` is continuous (hence
1022AE-strongly measurable on any finite interval). -/
1023theorem aestronglyMeasurable_galerkinForcing_mode_of_continuous
1024    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1025    (hBcont : ∀ N : ℕ,
1026      Continuous (fun p : GalerkinState N × GalerkinState N => (Bop N) p.1 p.2))
1027    (hucont : ∀ N : ℕ, Continuous (H.uN N))
1028    (N : ℕ) (t : ℝ) (_ht : 0 ≤ t) (k : Mode2) :
1029    MeasureTheory.AEStronglyMeasurable
1030      (fun s : ℝ => (galerkinForcing H Bop N s) k)
1031      (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)) := by
1032  -- Continuity of `s ↦ Bop N (uN N s) (uN N s)`.
1033  have hpair : Continuous fun s : ℝ => (H.uN N s, H.uN N s) := by
1034    -- build continuity from `ContinuousAt.prodMk`
1035    refine continuous_iff_continuousAt.2 ?_
1036    intro s
1037    simpa using
1038      (ContinuousAt.prodMk (x := s) ((hucont N).continuousAt) ((hucont N).continuousAt))