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

Scalar support with the canonical vector-field derivative gives zero box integral

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_fderiv · 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 DifferentiableAt ℝ G x. The scalar trace σ is integrable on K with respect to volume; this is an explicit premise. Function.support χ⊆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],\quad B(x)=\operatorname{fderiv}_{\mathbb R}G(x),\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, and ℓ:P→(P→L[ℝ]ℝ) are supplied. B(x) denotes canonical fderiv ℝ G x, not an additional parameter. Let H=χG, M(x)v=χ(x)B(x)v+ℓ(x)[v]G(x), and σ(x)=Σ_i(M(x)e_i)_i.
  • χ and G are continuous on K. At every x∈O∖s, HasFDerivAt χ (ℓ x) x and DifferentiableAt ℝ G x.
  • The scalar trace σ is integrable on K with respect to volume; this is an explicit premise.
  • Function.support χ⊆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. Turn differentiability of G into a canonical derivative witness

For x∈O∖s, DifferentiableAt ℝ G x certifies that fderiv ℝ G x is the actual Fréchet derivative. No formula for it is assumed away from that set.

\[x\in O\setminus s\Longrightarrow DG(x)=\operatorname{fderiv}_{\mathbb R}G(x).\]
Corresponding Lean step

fun x hx => (hGd x hx).hasFDerivAt.

2. Specialize the separate-regularity scalar-support theorem

Choose B=fderiv G in the existing regularity theorem. The assumed trace integrability already uses this canonical field, so all inputs match.

\[M(x)=\chi(x)\operatorname{fderiv}_{\mathbb R}G(x)+\ell(x)\otimes G(x),\qquad\int_K\delta(\chi G)\,dx=0.\]
Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_regularity ... (fun x => fderiv ℝ G x) ....

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_fderiv

This wrapper removes only the separately supplied vector derivative field G′, replacing it by canonical fderiv under actual differentiability. The scalar derivative field χ′ and trace-integrability premise remain.

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_scalar_support_subset_univ_pi_Ioo_of_fderiv
    {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) → ℝ)
    (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,
      DifferentiableAt ℝ G x)
    (Hi_trace : IntegrableOn
      (fun x => ∑ i, ((χ x • fderiv ℝ G x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume)
    (hχsupp : Function.support χ ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∫ 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_scalar_support_subset_univ_pi_Ioo_of_fderiv

The source first for x∈O∖s, DifferentiableAt ℝ G x certifies that fderiv ℝ G x is the actual Fréchet derivative. No formula for it is assumed away from that set. It finishes as follows: Choose B=fderiv G in the existing regularity theorem. The assumed trace integrability already uses this canonical field, so all inputs match. 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_scalar_support_subset_univ_pi_Ioo_of_fderiv
    {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) → ℝ)
    (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,
      DifferentiableAt ℝ G x)
    (Hi_trace : IntegrableOn
      (fun x => ∑ i, ((χ x • fderiv ℝ G x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume)
    (hχsupp : Function.support χ ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∫ 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_scalar_support_subset_univ_pi_Ioo_of_regularity
    a b hle χ χ' G (fun x => fderiv ℝ G x) s hs hχc hGc hχd
    (fun x hx => (hGd x hx).hasFDerivAt) Hi_trace hχsupp

/-- Scalar-support version of
`integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_trace_continuous`.

It uses closed-box continuity of the product-rule trace to discharge the
compact-box trace-integrability side condition, but remains only a finite-box
cutoff-smul handoff. -/

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)

  • DifferentiableAt.hasFDerivAt

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.