Samplinglib mathematical lesson
A compactly supported C¹ field has zero whole-space divergence integral
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport · theorem · Teaching coverage
Read this first
Mathematical statement
Let n∈ℕ and F:P→P be continuously differentiable on all raw P and have compact topological support. Then the whole-space Lebesgue integral of its PiLp-wrapped Euclidean coordinate divergence δF is zero.
\[F\in C^1(P,P),\quad\operatorname{tsupp}F\text{ compact}\quad\Longrightarrow\quad\int_P\operatorname{Div}(T\circ F\circ T^{-1})(Tx)\,dx=0.\]
Lean statement · integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
This is an existing whole-space theorem, unlike the earlier box-only wrappers. It uses exact compact support to remove the box, not a cutoff-exhaustion or tail-limit argument. C¹, rather than C∞, is the exact regularity premise.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
{n : ℕ}
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(hF : ContDiff ℝ 1 F)
(hF_support : HasCompactSupport F) :
∫ x : Fin (n + 1) → ℝ,
coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) = 0
Exact module and namespace context
Proof roadmap
- 1Enclose the closed support in a strict finite box
Compact support is bounded, so choose R>0 with tsupp F⊆B_P(0,R). Let a_i=−R and b_i=R. The coordinate bound |x_i|≤‖x‖∞ shows this raw-norm ball lies inside O=(-R,R)^d, and O⊆K=[−R,R]^d.
- 2Obtain an integrable trace from global C¹ regularity
C¹ regularity makes DF continuous. Evaluation at each fixed e_i and coordinate projection preserve continuity, and a finite sum makes τ_DF continuous. Thus its restriction to compact K is integrable.
- 3Apply the supported finite-box zero integral theorem
Global C¹ gives continuity on K and actual derivatives everywhere, so take the exceptional set to be empty. The support enclosure and trace integrability give ∫_K δF=0.
- 4Show the divergence is zero outside the containing box
If x∉K, the support enclosure implies x∉tsupp F. The field is locally zero there and therefore has zero Fréchet derivative. The pointwise transported trace theorem then gives δF(x)=0.
- 5Remove the box without taking a limit
The integrand is exactly zero at every point of the complement of K. Its whole-space integral equals its restricted integral, already proved zero.
Full assumptions and notation
All objects and hypotheses
- n∈ℕ, d=n+1≥1, P=(Fin d→ℝ) with its usual supremum norm, V=EuclideanSpace ℝ (Fin d) with its ℓ² norm. T:P→V is WithLp.toLp 2, a continuous linear equivalence, and e=T⁻¹=WithLp.ofLp.
- F:P→P; ContDiff ℝ 1 F globally; HasCompactSupport F, meaning the closure of {x:F(x)≠0} is compact.
- The integral is with respect to Lebesgue volume on raw P. No arbitrary measure, weight, density, or additional field occurs.
Mathematical proof
1. Enclose the closed support in a strict finite box
Compact support is bounded, so choose R>0 with tsupp F⊆B_P(0,R). Let a_i=−R and b_i=R. The coordinate bound |x_i|≤‖x‖∞ shows this raw-norm ball lies inside O=(-R,R)^d, and O⊆K=[−R,R]^d.
\[\operatorname{tsupp}F\subseteq B_P(0,R)\subseteq(-R,R)^d\subseteq[-R,R]^d,\qquad R>0.\]
Corresponding Lean step
hF_support.isCompact.isBounded.subset_ball_lt 0 0; norm_le_pi_norm x i; abs_lt.mp; construct a, b, hab, hball_open, hopen_closed.
2. Obtain an integrable trace from global C¹ regularity
C¹ regularity makes DF continuous. Evaluation at each fixed e_i and coordinate projection preserve continuity, and a finite sum makes τ_DF continuous. Thus its restriction to compact K is integrable.
\[x\mapsto DF(x)\text{ continuous}\Longrightarrow\tau_{DF}\in C^0(P)\Longrightarrow\tau_{DF}\in L^1(K,dx).\]
Corresponding Lean step
hF.continuous_fderiv one_ne_zero; .clm_apply continuous_const; continuous_apply; continuous_finsetSum; .integrableOn_compact isCompact_Icc.
3. Apply the supported finite-box zero integral theorem
Global C¹ gives continuity on K and actual derivatives everywhere, so take the exceptional set to be empty. The support enclosure and trace integrability give ∫_K δF=0.
\[\operatorname{supp}F\subseteq O,\quad s=\varnothing,\qquad\int_K\delta F\,dx=0.\]
Corresponding Lean step
integral_coordinateDivergence_toPi_box_eq_zero_of_support_subset_univ_pi_Ioo a b hab F (fun x => fderiv ℝ F x) ∅ Set.countable_empty; (hF.differentiable one_ne_zero x).hasFDerivAt.
4. Show the divergence is zero outside the containing box
If x∉K, the support enclosure implies x∉tsupp F. The field is locally zero there and therefore has zero Fréchet derivative. The pointwise transported trace theorem then gives δF(x)=0.
\[x\notin K\Longrightarrow x\notin\operatorname{tsupp}F\Longrightarrow DF(x)=0\Longrightarrow\delta F(x)=0.\]
Corresponding Lean step
HasFDerivAt.of_notMem_tsupport ℝ hxtsupport; coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt; simplify the zero trace.
5. Remove the box without taking a limit
The integrand is exactly zero at every point of the complement of K. Its whole-space integral equals its restricted integral, already proved zero.
\[\int_P\delta F\,dx=\int_K\delta F\,dx=0.\]
Corresponding Lean step
setIntegral_eq_integral_of_forall_compl_eq_zero; conclude with hbox.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
The source first compact support is bounded, so choose R>0 with tsupp F⊆B_P(0,R). Let a_i=−R and b_i=R. The coordinate bound |x_i|≤‖x‖∞ shows this raw-norm ball lies inside O=(-R,R)^d, and O⊆K=[−R,R]^d. It finishes as follows: The integrand is exactly zero at every point of the complement of K. Its whole-space integral equals its restricted integral, already proved zero. Intermediate steps below identify the actual helper calls and the conditions each one needs.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport
{n : ℕ}
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(hF : ContDiff ℝ 1 F)
(hF_support : HasCompactSupport F) :
∫ x : Fin (n + 1) → ℝ,
coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) = 0 := by
obtain ⟨R, hR, htsupport_ball⟩ :=
hF_support.isCompact.isBounded.subset_ball_lt 0
(0 : Fin (n + 1) → ℝ)
let a : Fin (n + 1) → ℝ := fun _ => -R
let b : Fin (n + 1) → ℝ := fun _ => R
have hab : a ≤ b := by
intro i
dsimp [a, b]
linarith
have hopen_closed :
(Set.univ.pi fun i => Set.Ioo (a i) (b i)) ⊆ Set.Icc a b := by
intro x hx
rw [Set.mem_pi] at hx
exact Set.mem_Icc.2 ⟨fun i => (hx i (Set.mem_univ i)).1.le,
fun i => (hx i (Set.mem_univ i)).2.le⟩
have hball_open : Metric.ball (0 : Fin (n + 1) → ℝ) R ⊆
(Set.univ.pi fun i => Set.Ioo (a i) (b i)) := by
intro x hxball
have hxnorm : ‖x‖ < R := by
simpa [Metric.mem_ball, dist_zero_right] using hxball
rw [Set.mem_pi]
intro i _hi
have hxi : |x i| < R := by
calc
|x i| = ‖x i‖ := (Real.norm_eq_abs _).symm
_ ≤ ‖x‖ := norm_le_pi_norm x i
_ < R := hxnorm
simpa [a, b] using (abs_lt.mp hxi)
have hsupport : Function.support F ⊆
(Set.univ.pi fun i => Set.Ioo (a i) (b i)) := by
intro x hx
exact hball_open (htsupport_ball (subset_tsupport F hx))
have htrace_cont : Continuous
(fun x : Fin (n + 1) → ℝ =>
∑ i, fderiv ℝ F x (Pi.single i (1 : ℝ)) i) := by
apply continuous_finsetSum
intro i _hi
exact (continuous_apply i).comp
(hF.continuous_fderiv one_ne_zero |>.clm_apply continuous_const)
have hbox :
∫ x in Set.Icc a b,
coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) = 0 := by
apply integral_coordinateDivergence_toPi_box_eq_zero_of_support_subset_univ_pi_Ioo
a b hab F (fun x => fderiv ℝ F x) ∅ Set.countable_empty
· exact hF.continuous.continuousOn
· intro x _hx
exact (hF.differentiable one_ne_zero x).hasFDerivAt
· exact htrace_cont.continuousOn.integrableOn_compact isCompact_Icc
· exact hsupport
calc
∫ x : Fin (n + 1) → ℝ,
coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) =
∫ x in Set.Icc a b,
coordinateDivergence
(fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
(WithLp.toLp 2 (F (WithLp.ofLp y)) :
EuclideanSpace ℝ (Fin (n + 1))))
(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) := by
symm
apply setIntegral_eq_integral_of_forall_compl_eq_zero
intro x hx
have hxtsupport : x ∉ tsupport F := by
intro hxt
exact hx (hopen_closed (hball_open (htsupport_ball hxt)))
have hzero := coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt
(ι := Fin (n + 1)) (HasFDerivAt.of_notMem_tsupport ℝ hxtsupport)
simpa using hzero
_ = 0 := hbox
end Divergence
end Calculus
end Analysis
end TechnicalLemmas
end AutoSamplingTheory
Exact module and namespace context
Scope and omitted-condition boundaries
- Whole-space no-boundary integral for one compactly supported C¹ field only; no weighted integration-by-parts identity, Gibbs law, semigroup, generator-domain or invariance assertion.
- The proof uses raw supremum-norm support enclosure and PiLp transport only in the divergence expression; it does not identify the two norms or apply a measure change.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Bornology.IsBounded.subset_ball_lt
- norm_le_pi_norm
- ContDiff.continuous_fderiv
- continuous_finsetSum
- ContinuousOn.integrableOn_compact
- HasFDerivAt.of_notMem_tsupport
- MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.