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

Off-box scalar vanishing with separate product regularity gives zero box integral

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

Statement

Let a≤b, χ:P→ℝ, G:P→P, and a countable s⊆P. χ and G are continuous on K. At every x∈O∖s, HasFDerivAt χ (ℓ x) x and HasFDerivAt G (B x) x. The scalar trace σ is integrable on K with respect to volume; this is an explicit premise. χ(x)=0 for every x∉O. Then the wrapped coordinate divergence of H=χG integrates to zero over K.

\[M(x)v=\chi(x)B(x)v+\ell(x)[v]G(x),\qquad \sigma(x)=\sum_i\left[\chi(x)(B(x)e_i)_i+\ell(x)[e_i]G_i(x)\right],\qquad\int_K\delta(\chi G)\,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.
  • a≤b coordinatewise; s⊆P is countable.
  • χ:P→ℝ, G:P→P, ℓ:P→(P→L[ℝ]ℝ), and B:P→(P→L[ℝ]P). Set M(x)=χ(x)B(x)+ℓ(x).smulRight(G(x)); thus M(x)v=χ(x)B(x)v+ℓ(x)[v]G(x). Set σ(x)=Σ_i(M(x)e_i)_i. Let H=χG.
  • χ and G are continuous on K. At every x∈O∖s, HasFDerivAt χ (ℓ x) x and HasFDerivAt G (B x) x.
  • The scalar trace σ is integrable on K with respect to volume; this is an explicit premise.
  • χ(x)=0 for every x∉O.

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. Assemble continuity of the product on the closed box

Continuity of scalar multiplication combines the separate continuity hypotheses to make H=χG continuous on K.

\[\chi,G\in C^0(K)\Longrightarrow H\in C^0(K).\]
Corresponding Lean step

continuousOn_smul_vectorField_of_continuousOn a b χ G hχc hGc.

2. Assemble its derivative on the good open set

At x∈O∖s, the two supplied derivatives give the product derivative M(x)=χ(x)B(x)+ℓ(x).smulRight(G(x)).

\[D H(x)[v]=\chi(x)B(x)[v]+\ell(x)[v]G(x)\qquad(x\in O\setminus s).\]
Corresponding Lean step

hasFDerivAt_smul_vectorField_off_countable a b χ χ' G G' s hχd hGd.

3. Use the product-level support-to-zero integral theorem

The preceding two steps supply the product's regularity. The existing theorem uses the given scalar support/vanishing condition and the still-assumed σ integrability to cancel the box integral.

\[\operatorname{supp}H\subseteq O,\quad\sigma\in L^1(K)\Longrightarrow\int_K\delta H\,dx=0.\]
Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo a b hle χ G (fun x => χ x • G' x + (χ' x).smulRight (G x)) ...

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_regularity

This theorem derives product-level continuity and derivative witnesses from the two factors. It does not derive trace integrability; that remains the Hi_trace parameter.

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_cutoff_eq_zero_off_univ_pi_Ioo_of_regularity
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hχd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hGd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x)
    (Hi_trace : IntegrableOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume)
    (hχzero : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 ((χ (WithLp.ofLp y)) • G (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_cutoff_eq_zero_off_univ_pi_Ioo_of_regularity

The source first continuity of scalar multiplication combines the separate continuity hypotheses to make H=χG continuous on K. It finishes as follows: The preceding two steps supply the product's regularity. The existing theorem uses the given scalar support/vanishing condition and the still-assumed σ integrability to cancel the 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_cutoff_eq_zero_off_univ_pi_Ioo_of_regularity
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hχd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hGd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x)
    (Hi_trace : IntegrableOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume)
    (hχzero : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 ((χ (WithLp.ofLp y)) • G (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_cutoff_eq_zero_off_univ_pi_Ioo
    a b hle χ G (fun x => χ x • G' x + (χ' x).smulRight (G x)) s hs
    (continuousOn_smul_vectorField_of_continuousOn a b χ G hχc hGc)
    (hasFDerivAt_smul_vectorField_off_countable a b χ χ' G G' s hχd hGd)
    Hi_trace hχzero

/-- Finite-box coordinate-divergence integral vanishes for a cutoff-smul vector
field when the scalar cutoff vanishes outside the open Pi-box, deriving the
regularity hypotheses from separate cutoff/vector-field assumptions and deriving
the product-rule trace integrability from a closed-box trace-continuity
hypothesis.

This closes only the compact-box trace-integrability side condition for the
cutoff-smul route.  It still does not construct a smooth cutoff, prove tail
limits, whole-space weighted IBP, generator domains, invariant laws,
reversibility, or KL/FI. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Finite-box zero integral only; no whole-space passage or invariant-law conclusion.
  • The support/vanishing assumption is imposed on χ; no value-one plateau or range [0,1] assumption is needed in this theorem.

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.