abs_heatFactor_le_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the bound when ν or τ is negative.
- Does not apply outside 2D Fourier modes.
- Does not quantify decay rates beyond the unit bound.
- Does not address integrability or measurability questions.
formal statement (Lean)
706lemma abs_heatFactor_le_one (ν : ℝ) (hν : 0 ≤ ν) (τ : ℝ) (hτ : 0 ≤ τ) (k : Mode2) :
707 |heatFactor ν τ k| ≤ 1 := by
proof body
Tactic-mode proof.
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
737 h_bound := by
738 refine Filter.Eventually.of_forall ?_
739 intro N
740 exact MeasureTheory.ae_of_all _ (fun s hs => h_bound N s hs)
741 bound_integrable := bound_integrable
742 h_lim := by
743 exact MeasureTheory.ae_of_all _ (fun s hs => h_lim s hs) }
744
745/-- Convert a forcing-level dominated convergence hypothesis into the kernel-level one. -/