abs_heatFactor_le_one

formal source

 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
 719
 720/-- Convenience constructor: it is often easier to assume pointwise statements (`∀`) rather than
 721almost-everywhere (`∀ᵐ`). This helper upgrades pointwise bounds + convergence to the AE versions
 722required by `ForcingDominatedConvergenceAt`. -/
 723noncomputable def ForcingDominatedConvergenceAt.of_forall
 724    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2)
 725    (bound : ℝ → ℝ)
 726    (h_meas : ∀ N : ℕ,
 727      MeasureTheory.AEStronglyMeasurable
 728        (fun s : ℝ => F_N N s k)
 729        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)))
 730    (h_bound : ∀ N : ℕ, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t → ‖F_N N s k‖ ≤ bound s)
 731    (bound_integrable : IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t)
 732    (h_lim : ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
 733      Tendsto (fun N : ℕ => F_N N s k) atTop (𝓝 (F s k))) :
 734    ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k :=
 735  { bound := bound
 736    h_meas := Filter.Eventually.of_forall h_meas