Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

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

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.\]

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 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

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.

Source and reuse

ASTIS 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

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.