Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Off-box scalar vanishing with continuous product trace gives zero box integral

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

Read this first

Mathematical 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 entire scalar trace σ is continuous on K; its integrability is derived, not assumed. χ(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.\]
Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_trace_continuous

Only continuity of the whole trace is added in place of an explicit integrability input. The theorem still requires separate factor regularity and the stated support/vanishing condition.

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.

Download module (.lean)
theorem integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_trace_continuous
    {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)
    (htrace : ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b))
    (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

Proof roadmap

  1. 1Use compactness of K to obtain trace integrability

    The trace σ is continuous by hypothesis and K is compact, so σ is integrable on K.

  2. 2Apply the separate-regularity zero integral theorem

    That integrability discharges exactly the missing input of the existing regularity theorem. The separate derivative and continuity premises and the scalar support condition are unchanged.

Full assumptions and notation

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 entire scalar trace σ is continuous on K; its integrability is derived, not assumed.
  • χ(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. Use compactness of K to obtain trace integrability

The trace σ is continuous by hypothesis and K is compact, so σ is integrable on K.

\[\sigma\in C^0(K),\quad K\text{ compact}\Longrightarrow\sigma\in L^1(K).\]
Corresponding Lean step

integrableOn_smul_vectorField_trace_of_continuousOn a b χ χ' G G' htrace.

2. Apply the separate-regularity zero integral theorem

That integrability discharges exactly the missing input of the existing regularity theorem. The separate derivative and continuity premises and the scalar support condition are unchanged.

\[\int_K\delta(\chi G)\,dx=0.\]
Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_regularity ...

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_trace_continuous

The source first the trace σ is continuous by hypothesis and K is compact, so σ is integrable on K. It finishes as follows: That integrability discharges exactly the missing input of the existing regularity theorem. The separate derivative and continuity premises and the scalar support condition are unchanged. 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.

Download module (.lean)
theorem integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo_of_trace_continuous
    {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)
    (htrace : ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b))
    (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_of_regularity
    a b hle χ χ' G G' s hs hχc hGc hχd hGd
    (integrableOn_smul_vectorField_trace_of_continuousOn a b χ χ' G G' htrace)
    hχzero

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

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