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

Zero updated-endpoint components give zero box divergence integral

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_toPi_box_eq_zero_of_update_boundary_component_eq_zero · theorem · Teaching coverage

Statement

Let a≤b and let F:P→P be continuous on K, have derivative A(x) at each x∈O∖s for a countable s, and have integrable trace τ_A on K. Assume additionally: For every i and every x∈P, F_i(x[i←b_i])=0 and F_i(x[i←a_i])=0. Then the integral of δF over K is zero.

\[\int_K\delta F(x)\,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.
  • a,b∈P; K=[a,b]={x:∀i,a_i≤x_i≤b_i} is the closed box and O=∏_i(a_i,b_i) is the open box. All unspecified integrals and a.e. assertions use Lebesgue volume on P, restricted to K when indicated.
  • F:P→P and A:P→(P→L[ℝ]P) is a supplied linear-map field. Write δF(x)=Div(T∘F∘T⁻¹)(Tx) and τ_A(x)=Σ_i(A(x)e_i)_i.
  • a≤b coordinatewise (zero-width coordinates are allowed).
  • s⊆P is countable; F is continuous on K; for every x∈O∖s, HasFDerivAt F (A x) x.
  • τ_A is integrable on K with respect to volume.
  • For each i, K_hat_i=∏_{j≠i}[a_j,b_j] is parametrized by Fin n→ℝ; I_i^c inserts c in coordinate i, retaining the other coordinates in their original order. Φ_a,b(F) is the sum of upper-face integrals of F_i minus lower-face integrals of F_i.
  • For every i and every x∈P, F_i(x[i←b_i])=0 and F_i(x[i←a_i])=0.

Notation and interpretation

Notation used below

For a raw field F:P→P, W_F=T∘F∘T⁻¹ and δF(x) is coordinateDivergence W_F at Tx. For a supplied linear-map field A, τ_A is its coordinate trace.

\[W_F:=T\circ F\circ T^{-1},\qquad\delta F(x):=\operatorname{Div}W_F(Tx),\qquad\tau_A(x):=\sum_i(A(x)e_i)_i.\]

Mathematical proof

1. Produce the zero signed face sum

Inserted endpoint vectors already have the updated coordinate, so the update hypotheses imply all inserted-face normal components vanish. Their face integrals, and hence Φ, vanish.

\[\forall i,x,\ F_i(x[i\leftarrow b_i])=F_i(x[i\leftarrow a_i])=0\Longrightarrow\Phi_{a,b}(F)=0.\]
Corresponding Lean step

signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero a b F with the stated boundary/support premises.

2. Combine with the conditional zero-face theorem

The original regularity and trace-integrability data satisfy the finite-box divergence theorem. Its zero-face corollary uses the just-proved Φ=0 to give the zero box integral.

\[\int_K\delta F\,dx=\Phi_{a,b}(F)=0.\]
Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_integrableOn_trace_of_hasFDerivAt_off_countable a b hle F F' s hs Hc Hd Hi_trace (...).

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_update_boundary_component_eq_zero

The derivative field F′ is supplied and is required to be correct only on O∖s. The chosen boundary/support premise replaces hfaces, but does not replace any regularity or integrability 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_toPi_box_eq_zero_of_update_boundary_component_eq_zero
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (F' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (Hc : ContinuousOn F (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (b i)) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (a i)) i = 0) :
    ∫ 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

Exact module and namespace context

Lean proof · integral_coordinateDivergence_toPi_box_eq_zero_of_update_boundary_component_eq_zero

The source first inserted endpoint vectors already have the updated coordinate, so the update hypotheses imply all inserted-face normal components vanish. Their face integrals, and hence Φ, vanish. It finishes as follows: The original regularity and trace-integrability data satisfy the finite-box divergence theorem. Its zero-face corollary uses the just-proved Φ=0 to give the zero box integral. 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_toPi_box_eq_zero_of_update_boundary_component_eq_zero
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (F' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (Hc : ContinuousOn F (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (b i)) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (a i)) i = 0) :
    ∫ 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
  exact integral_coordinateDivergence_toPi_box_eq_zero_of_integrableOn_trace_of_hasFDerivAt_off_countable
    a b hle F F' s hs Hc Hd Hi_trace
    (signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero a b F hupper hlower)

/-- Finite-box coordinate-divergence integral vanishes when the vector field
vanishes outside the open Pi-box.

This is still a finite-box conditional theorem: it assumes the trace
integrability and open-box/off-countable differentiability required by the
divergence theorem wrapper.  It does not pass to whole space, prove compact
support or tail decay, or state stationarity/invariance. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Only the finite box K is integrated. No passage to whole space, weighted integration by parts, generator domain, stationary law, or invariance follows from this wrapper alone.
  • Derivative values at the boundary and on the countable exceptional set are not prescribed; equality of integrands is used a.e.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

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.