ForcingDominatedConvergenceAt

formal source

 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`. -/
 688structure ForcingDominatedConvergenceAt
 689    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2) where
 690  bound : ℝ → ℝ
 691  h_meas :
 692    ∀ᶠ N : ℕ in atTop,
 693      MeasureTheory.AEStronglyMeasurable
 694        (fun s : ℝ => F_N N s k)
 695        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 696  h_bound :
 697    ∀ᶠ N : ℕ in atTop,
 698      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t → ‖F_N N s k‖ ≤ bound s
 699  bound_integrable :
 700    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 701  h_lim :
 702    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 703      Tendsto (fun N : ℕ => F_N N s k) atTop (𝓝 (F s k))
 704
 705/-- Heat kernel bound: for `ν ≥ 0` and `τ ≥ 0`, we have `|heatFactor ν τ k| ≤ 1`. -/
 706lemma abs_heatFactor_le_one (ν : ℝ) (hν : 0 ≤ ν) (τ : ℝ) (hτ : 0 ≤ τ) (k : Mode2) :
 707    |heatFactor ν τ k| ≤ 1 := by
 708  -- `heatFactor = exp (-ν * kSq k * τ)` with a nonpositive exponent.
 709  have hkSq : 0 ≤ kSq k := by simp [kSq, add_nonneg, sq_nonneg]
 710  have harg : (-ν * kSq k * τ) ≤ 0 := by
 711    have hprod : 0 ≤ ν * kSq k * τ := mul_nonneg (mul_nonneg hν hkSq) hτ
 712    -- `-x ≤ 0` for `x ≥ 0`
 713    have : -(ν * kSq k * τ) ≤ 0 := neg_nonpos.mpr hprod
 714    simpa [mul_assoc, mul_left_comm, mul_comm] using this
 715  have hle : heatFactor ν τ k ≤ 1 := by
 716    simpa [heatFactor] using (Real.exp_le_one_iff.2 harg)
 717  have hnonneg : 0 ≤ heatFactor ν τ k := (Real.exp_pos _).le
 718  simpa [abs_of_nonneg hnonneg] using hle