of_convectionNormBound

formal source

1052
1053This discharges the `bound_integrable` and `dom` fields of `GalerkinForcingDominatedConvergenceHypothesis`,
1054leaving only measurability + pointwise forcing convergence as hypotheses. -/
1055noncomputable def of_convectionNormBound
1056    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1057    (C : ℝ) (hC : 0 ≤ C)
1058    (hB : ∀ N : ℕ, ∀ u : GalerkinState N, ‖(Bop N u u)‖ ≤ C * ‖u‖ ^ 2)
1059    (F : ℝ → FourierState2D)
1060    (meas : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
1061      MeasureTheory.AEStronglyMeasurable
1062        (fun s : ℝ => (galerkinForcing H Bop N s) k)
1063        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)))
1064    (lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1065      Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))) :
1066    GalerkinForcingDominatedConvergenceHypothesis H Bop :=
1067by
1068  classical
1069  refine
1070    { F := F
1071      bound := fun _t _k _s => C * H.B ^ 2
1072      bound_integrable := by
1073        intro t _ht k
1074        -- constant function is interval integrable on any finite interval
1075        simp
1076      meas := meas
1077      dom := ?_
1078      lim := lim }
1079  intro N t ht k s hs
1080  -- from `s ∈ uIoc 0 t` and `0 ≤ t`, we have `0 < s` hence `0 ≤ s`.
1081  have hs' : 0 < s ∧ s ≤ t := by
1082    have hs'' : min (0 : ℝ) t < s ∧ s ≤ max (0 : ℝ) t := by
1083      simpa [Set.uIoc, Set.mem_Ioc] using hs
1084    simpa [min_eq_left ht, max_eq_right ht] using hs''
1085  have hs0 : 0 ≤ s := le_of_lt hs'.1