abs_heatFactor_le_one
plain-language theorem explainer
The lemma proves that the heat factor exp(-ν |k|^2 τ) for any 2D Fourier mode k satisfies |heatFactor| ≤ 1 whenever viscosity ν and time τ are nonnegative. Analysts passing from Galerkin truncations to continuum limits in 2D fluids cite it to justify the dominated-convergence step inside the Duhamel formula. The tactic proof reduces the claim to the elementary inequality exp(x) ≤ 1 for x ≤ 0 together with positivity of the exponential.
Claim. For all real numbers $ν ≥ 0$, $τ ≥ 0$ and every 2D Fourier mode $k ∈ ℤ × ℤ$, $|exp(-ν |k|^2 τ)| ≤ 1$.
background
The ContinuumLimit2D module constructs a Lean-verifiable path from finite-dimensional Galerkin approximations of 2D fluids to a continuum Fourier-state limit. Central objects include the heat factor defined by heatFactor ν τ k := Real.exp(-ν * kSq k * τ), where kSq k := k₁² + k₂² for mode k = (k₁, k₂). The structure ForcingDominatedConvergenceAt packages pointwise bounds and convergence hypotheses at fixed time t and mode k; its doc-comment states that the present bound upgrades such hypotheses to the kernel-level version required by DuhamelKernelDominatedConvergenceAt.
proof idea
The proof first verifies kSq k ≥ 0 by add_nonneg and sq_nonneg. It then shows the product ν kSq k τ is nonnegative, hence its negation is nonpositive. Real.exp_le_one_iff applied to this argument yields heatFactor ≤ 1. Nonnegativity of the exponential (from Real.exp_pos) lets the absolute value be replaced by the value itself, completing the bound.
why it matters
This bound is invoked inside duhamelKernelDominatedConvergenceAt_of_forcing to convert a forcing-level dominated-convergence hypothesis into the corresponding kernel-level statement. It therefore supplies one of the analytic estimates needed to close the continuum-limit pipeline at milestone M5. In the Recognition framework the result sits inside the classical-bridge layer that recovers continuum fluid equations from the underlying discrete structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.