integral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupport

Plain-English statement

The integral over the whole finite-dimensional space of the divergence of a continuously differentiable compactly supported vector field is zero.

Scope guard. This card records a compiled local declaration. Its mathematical scope is exactly the Lean statement below; the Registry note and source correspondence may describe motivation but do not strengthen it.

Mathematical statement

If F is C1 with compact support on R^d, then integral div F dx = 0.

Intuition

A compactly supported field has no flux at infinity. ASTIS makes that sentence precise by enclosing its topological support in a strict finite box and applying the finite-box divergence theorem where every face value is zero.

Conditions

The coordinate index is finite and nonempty in the current Fin (n+1) interface.
The vector field is globally C1.
The vector field has compact topological support.

Why these conditions cannot be dropped

C1 regularity gives a genuine Frechet derivative and a continuous, hence box-integrable, derivative trace.
Compact support supplies an actual zero-boundary region rather than an informal decay-at-infinity claim.
Finite dimension is required by the current Mathlib box divergence theorem and PiLp coordinate trace.

Proof route

Use compactness to place tsupport F inside an open norm ball and then a strict Pi-box.
Derive continuity and integrability of the canonical fderiv trace from ContDiff C1.
Invoke the ASTIS finite-box zero-face divergence wrapper.
Outside the closed box, use the zero local germ off tsupport F to show fderiv F and the wrapped divergence vanish.
Rewrite the closed-box integral as the whole-space integral.

Lean interface notes

The theorem explicitly bridges raw finite-Pi coordinates and EuclideanSpace through WithLp.
HasCompactSupport controls tsupport, which is stronger and topologically more stable than a bare Function.support bound.
The declaration is independent of Gibbs measures and can be reused by other conservation-law proofs.

Lean learning studio · mathematics → formal proof

Read the mathematics first, then descend into Lean

You do not need to know Lean before opening this panel. The page keeps the paper-level theorem, rigorous proof obligations, exact Lean declaration, and proof dependencies as separate layers so a first-time reader can move down one layer at a time.

BeginnerWhy this theorem exists → intuition → statement → one hand calculation. Hide proof-engineering detail.

RigorousExpose assumptions, hidden measure/limit/domain issues, proof route, and rigorous references.

Lean learnerOpen the exact declaration, proof tree/network, syntax glossary, and line-by-line explanation.

Proof architecture

Start with the tree when learning: prerequisites sit below the theorem and downstream results sit above it. Switch to the network when you want to understand where this declaration lives in the local formal library. Every mapped node is clickable.

Loading source-derived dependency evidence…

Graph rule: only dependencies found by the ASTIS source scan are drawn. Missing tactic indirection is treated as an under-approximation; the site never invents an edge just to make a prettier graph.

How to read the exact Lean declaration

Read a Lean theorem left-to-right exactly as you would unpack a mathematical sentence: name → ambient types → automatically inferred structures → explicit hypotheses → conclusion → proof. Then read the proof top-to-bottom as transformations of the current goal.

NameWhat reusable mathematical fact is being created?
ParametersWhich symbols are arbitrary, and which structures are inferred by typeclass search?
PropositionAfter the colon, translate the Lean expression back into a paper statement.
Proof actionsAfter by, ask what each tactic does to the mathematical goal—not only what syntax it uses.

Syntax used on this page

This glossary is filtered to syntax that actually occurs in the declaration above. Open a symbol only when you meet it, rather than memorizing Lean grammar in advance.

Source voice and ASTIS voice stay separate

When Samplinglib shows a short quotation from Chewi, it is labeled as a source excerpt and linked to the canonical book page. Intuition, expanded proof steps, hidden regularity assumptions, and Lean explanations are ASTIS-authored commentary. A quotation never substitutes for a formal proof, and an ASTIS explanation is never attributed to the textbook author.

Lean statement

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

Open AutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Divergence.lean:1794published source at 7bcd37294df1