structure
definition
DuhamelKernelDominatedConvergenceAt
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 660.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
FourierState2D -
heatFactor -
Mode2 -
restrict -
kernel -
of -
A -
of -
of -
for -
kernel -
of -
A -
A -
and -
volume -
F -
F -
F -
interval
used by
-
duhamelKernelDominatedConvergenceAt_of_forcing -
nsDuhamelCoeffBound -
nsDuhamelCoeffBound_galerkinKernel -
nsDuhamelCoeffBound_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
tendsto_duhamelKernelIntegral_of_dominated_convergence -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel
formal source
657
658/-- Hypothesis (at fixed `t,k`): the Duhamel-kernel integrands satisfy the assumptions of dominated
659convergence, so the corresponding interval integrals converge. -/
660structure DuhamelKernelDominatedConvergenceAt
661 (ν : ℝ) (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
662 (t : ℝ) (k : Mode2) where
663 /-- An `L¹` bound for the integrands on `0..t`. -/
664 bound : ℝ → ℝ
665 /-- Strong measurability (eventually in `N`) on the relevant interval. -/
666 h_meas :
667 ∀ᶠ N : ℕ in atTop,
668 MeasureTheory.AEStronglyMeasurable
669 (fun s : ℝ => (heatFactor ν (t - s) k) • (F_N N s k))
670 (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
671 /-- Dominating bound (eventually in `N`) on the relevant interval. -/
672 h_bound :
673 ∀ᶠ N : ℕ in atTop,
674 ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
675 ‖(heatFactor ν (t - s) k) • (F_N N s k)‖ ≤ bound s
676 /-- Integrability of the bound. -/
677 bound_integrable :
678 IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
679 /-- Pointwise (ae on the interval) convergence of the integrands. -/
680 h_lim :
681 ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
682 Tendsto (fun N : ℕ => (heatFactor ν (t - s) k) • (F_N N s k)) atTop
683 (𝓝 ((heatFactor ν (t - s) k) • (F s k)))
684
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 : ℝ → ℝ