Pointwise trace transport on an almost-everywhere differentiability set
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_wrapped_toPi_trace_ae_of_ae_hasFDerivAt · theorem · Teaching coverage
Mathematical statement
For raw P, endpoints a,b, F:P→P and derivative field A, if F has derivative A(x) for almost every x under volume restricted to K, then δF=τ_A almost everywhere on that same restricted measure.
Lean statement · coordinateDivergence_wrapped_toPi_trace_ae_of_ae_hasFDerivAt
This wrapper consumes an a.e. derivative hypothesis directly; it does not establish one from boundary or countability arguments.
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_ae_hasFDerivAt
{n : ℕ}
(a b : Fin (n + 1) → ℝ)
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(F' : (Fin (n + 1) → ℝ) →
(Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
(hF_ae : ∀ᵐ x ∂volume.restrict (Set.Icc a b), 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 : ℝ)) iProof roadmap
- 1Apply the pointwise identity where its hypothesis holds
On the full-measure set of derivative points, the already-proved transport theorem identifies the two real values. Consequently the functions agree a.e. on K.
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.
- 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.
- HasFDerivAt F (A x) x for volume|K-almost every x; no a≤b 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. Apply the pointwise identity where its hypothesis holds
On the full-measure set of derivative points, the already-proved transport theorem identifies the two real values. Consequently the functions agree a.e. on K.
Corresponding Lean step
filter_upwards [hF_ae]; coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt hx.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · coordinateDivergence_wrapped_toPi_trace_ae_of_ae_hasFDerivAt
On the full-measure set of derivative points, the already-proved transport theorem identifies the two real values. Consequently the functions agree a.e. on K. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.
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_ae_hasFDerivAt
{n : ℕ}
(a b : Fin (n + 1) → ℝ)
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(F' : (Fin (n + 1) → ℝ) →
(Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
(hF_ae : ∀ᵐ x ∂volume.restrict (Set.Icc a b), 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 := by
filter_upwards [hF_ae] with x hx
exact coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt (ι := Fin (n + 1)) hxScope and omitted-condition boundaries
- A.e. equality alone is not integrability.
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
- Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
- Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
- Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
- Existing focused test — Exact named declaration invocation located in an existing example; no test was run.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.