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

Obtain the a.e. trace bridge from derivatives off a countable set

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

Statement

For endpoints a,b, F:P→P and derivative field A, suppose s⊆P is countable and F has derivative A(x) at every x∈O∖s. Then δF=τ_A almost everywhere on K with respect to restricted volume.

\[DF=A\text{ on }O\setminus s,\ s\text{ countable}\quad\Longrightarrow\quad\delta F=\tau_A\quad\text{a.e. on }K.\]

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.
  • s⊆P is countable; HasFDerivAt F (A x) x at every x∈O∖s. No endpoint-order, continuity or integrability assumption.

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. Identify values in the open good set

At each x∈O∖s, apply the pointwise transported trace identity to the supplied derivative.

\[\delta F(x)=\tau_A(x)\qquad(x\in O\setminus s).\]
Corresponding Lean step

coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt (Hd x hx).

2. Transfer equality to the restricted closed box

Use the preceding null-boundary/countable-exception transfer theorem to extend this equality in the a.e. sense to K.

\[\delta F=\tau_A\quad\text{a.e. }[dx|_K].\]
Corresponding Lean step

eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable hs.

Lean statement · coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable

The name 'off_countable' corresponds to an actual `hs : s.Countable` parameter here. Values of the derivative field on the exceptional set need not be specified by differentiation.

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 coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (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)
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x) :
      (fun x => 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))))
      =ᵐ[volume.restrict (Set.Icc a b)]
      fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i

Exact module and namespace context

Lean proof · coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable

The source first at each x∈O∖s, apply the pointwise transported trace identity to the supplied derivative. It finishes as follows: Use the preceding null-boundary/countable-exception transfer theorem to extend this equality in the a.e. sense to K. 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 coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (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)
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x) :
      (fun x => 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))))
      =ᵐ[volume.restrict (Set.Icc a b)]
      fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i :=
  eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable
    (a := a) (b := b) (s := s) hs fun x hx =>
      coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt (ι := Fin (n + 1)) (Hd x hx)

/-- Transfer box integrability from Mathlib's Pi-space trace summand to the
ASTIS wrapped coordinate-divergence integrand.

This closes only the representation mismatch between the two integrands.  The
trace integrability hypothesis is still an explicit analytic assumption; this
theorem does not prove integrability of any concrete Langevin vector field,
weighted IBP, boundary cancellation, generator domains, or invariant-law
consequences. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No differentiability on the box boundary is required.

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.