def
definition
def or abbrev
duhamelKernelDominatedConvergenceAt_of_forcing
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Definition body.
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
777 intro hs
778 have hst : 0 < s ∧ s ≤ t := by
779 -- unpack membership in the unordered interval
780 have hs' : min (0 : ℝ) t < s ∧ s ≤ max (0 : ℝ) t := by
781 simpa [Set.uIoc, Set.mem_Ioc] using hs
782 simpa [min_eq_left ht, max_eq_right ht] using hs'
783 have hts : 0 ≤ t - s := sub_nonneg.mpr hst.2
784 have habs : |heatFactor ν (t - s) k| ≤ 1 :=
785 abs_heatFactor_le_one ν hν (t - s) hts k
786 have hx : ‖F_N N s k‖ ≤ hF.bound s := hsBound hs
787 calc
788 ‖(heatFactor ν (t - s) k) • (F_N N s k)‖
789 = |heatFactor ν (t - s) k| * ‖F_N N s k‖ := by
790 simp [Real.norm_eq_abs, norm_smul]
791 _ ≤ ‖F_N N s k‖ := by
792 simpa [one_mul] using (mul_le_of_le_one_left (norm_nonneg _) habs)
793 _ ≤ hF.bound s := hx
794 · -- pointwise convergence: multiply by the (fixed-in-`N`) scalar `heatFactor ν (t-s) k`
795 filter_upwards [hF.h_lim] with s hsLim
796 intro hs
797 have hcont : Continuous fun v : VelCoeff => (heatFactor ν (t - s) k) • v := continuous_const_smul _
798 exact (hcont.tendsto (F s k)).comp (hsLim hs)
799
800/-- Under the dominated-convergence hypothesis at `t,k`, the Duhamel-kernel integrals converge. -/