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

Transport the raw-coordinate trace to Euclidean divergence

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

Statement

Let ι be finite, P=(ι→ℝ), V=EuclideanSpace ℝ ι, T:P≃L[ℝ]V the canonical coordinate conversion, and W_F=T∘F∘T⁻¹. If F:P→P has Fréchet derivative A:P→L[ℝ]P at x∈P, then Div W_F(Tx)=Σ_i(Ae_i)_i in raw coordinates.

\[DF(x)=A\quad\Longrightarrow\quad\operatorname{Div}(T\circ F\circ T^{-1})(Tx)=\sum_i(Ae_i^P)_i.\]

All objects and hypotheses

  • ι is finite with Fintype and DecidableEq; P has its supremum norm and V its ℓ² norm.
  • F:P→P, A:P→L[ℝ]P, x∈P and HasFDerivAt F A x.

Mathematical proof

1. Transport the derivative through both linear conversions

The derivative of T⁻¹ is T⁻¹ and the derivative of T is T. Two chain-rule applications give D W_F(Tx)=T∘A∘T⁻¹.

\[D W_F(Tx)=T\circ A\circ T^{-1}.\]
Corresponding Lean step

PiLp.hasFDerivAt_ofLp; PiLp.hasFDerivAt_toLp; hF.comp ... hofLp; htoLp.comp ... hF_ofLp.

2. Take the Euclidean coordinate trace

The existing pointwise trace theorem applies to this genuine derivative of W_F.

\[\operatorname{Div}W_F(Tx)=\sum_i\bigl(T A T^{-1}e_i^V\bigr)_i.\]
Corresponding Lean step

coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt hwrapped.

3. Cancel coordinate representations in each summand

T⁻¹ sends e_i^V to e_i^P and T preserves coordinate values. Thus each summand becomes (Ae_i^P)_i.

\[T^{-1}e_i^V=e_i^P,\qquad(Tv)_i=v_i.\]
Corresponding Lean step

continuousLinearEquiv_apply_euclideanSpace_single; ContinuousLinearMap.comp_apply; Finset.sum_congr.

Lean statement · coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt

The conclusion evaluates Euclidean divergence at Tx but retains an ordinary raw-Pi trace on the right. It is a pointwise representation bridge, not a measure transport theorem.

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_of_hasFDerivAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : (ι → ℝ) → ι → ℝ}
    {F' : (ι → ℝ) →L[ℝ] (ι → ℝ)}
    {x : ι → ℝ}
    (hF : HasFDerivAt F F' x) :
    coordinateDivergence
        (fun y : EuclideanSpace ℝ ι =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) : EuclideanSpace ℝ ι))
        (WithLp.toLp 2 x : EuclideanSpace ℝ ι) =
      ∑ i, F' (Pi.single i (1 : ℝ)) i

Exact module and namespace context

Lean proof · coordinateDivergence_wrapped_toPi_trace_of_hasFDerivAt

The source first the derivative of T⁻¹ is T⁻¹ and the derivative of T is T. Two chain-rule applications give D W_F(Tx)=T∘A∘T⁻¹. It finishes as follows: T⁻¹ sends e_i^V to e_i^P and T preserves coordinate values. Thus each summand becomes (Ae_i^P)_i. 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_of_hasFDerivAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : (ι → ℝ) → ι → ℝ}
    {F' : (ι → ℝ) →L[ℝ] (ι → ℝ)}
    {x : ι → ℝ}
    (hF : HasFDerivAt F F' x) :
    coordinateDivergence
        (fun y : EuclideanSpace ℝ ι =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) : EuclideanSpace ℝ ι))
        (WithLp.toLp 2 x : EuclideanSpace ℝ ι) =
      ∑ i, F' (Pi.single i (1 : ℝ)) i := by
  let e : EuclideanSpace ℝ ι ≃L[ℝ] (ι → ℝ) :=
    PiLp.continuousLinearEquiv 2 ℝ (fun _ : ι => ℝ)
  have hofLp : HasFDerivAt (fun y : EuclideanSpace ℝ ι => WithLp.ofLp y)
      e.toContinuousLinearMap (WithLp.toLp 2 x : EuclideanSpace ℝ ι) := by
    simpa [e] using
      (PiLp.hasFDerivAt_ofLp (𝕜 := ℝ) (E := fun _ : ι => ℝ) 2
        (WithLp.toLp 2 x : EuclideanSpace ℝ ι))
  have hF_ofLp : HasFDerivAt (fun y : EuclideanSpace ℝ ι => F (WithLp.ofLp y))
      (F'.comp e.toContinuousLinearMap) (WithLp.toLp 2 x : EuclideanSpace ℝ ι) := by
    simpa [Function.comp_def] using hF.comp (WithLp.toLp 2 x : EuclideanSpace ℝ ι) hofLp
  have htoLp : HasFDerivAt (fun z : ι → ℝ =>
        (WithLp.toLp 2 z : EuclideanSpace ℝ ι))
      e.symm.toContinuousLinearMap (F x) := by
    simpa [e] using
      (PiLp.hasFDerivAt_toLp (𝕜 := ℝ) (E := fun _ : ι => ℝ) 2 (F x))
  have hwrapped : HasFDerivAt
      (fun y : EuclideanSpace ℝ ι =>
        (WithLp.toLp 2 (F (WithLp.ofLp y)) : EuclideanSpace ℝ ι))
      (e.symm.toContinuousLinearMap.comp (F'.comp e.toContinuousLinearMap))
      (WithLp.toLp 2 x : EuclideanSpace ℝ ι) := by
    simpa [Function.comp_def] using htoLp.comp (WithLp.toLp 2 x : EuclideanSpace ℝ ι)
      hF_ofLp
  have htrace := coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt hwrapped
  trans ∑ i, (e.symm.toContinuousLinearMap.comp (F'.comp e.toContinuousLinearMap))
      (EuclideanSpace.single i (1 : ℝ)) i
  · exact htrace
  · refine Finset.sum_congr rfl ?_
    intro i _hi
    have hsingle : e (EuclideanSpace.single i (1 : ℝ)) = Pi.single i (1 : ℝ) := by
      simpa [e] using continuousLinearEquiv_apply_euclideanSpace_single (ι := ι) i
    simp [ContinuousLinearMap.comp_apply, hsingle, e]

/-- If two functions on a finite-dimensional box agree on the open box away
from a countable exceptional set, then they agree a.e. on the closed box with
respect to restricted volume.

This is a reusable measure-theoretic transfer leaf.  It packages Mathlib's
fact that the open Pi-box is a.e. equal to the closed Pi-box, plus countable
sets have zero volume. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No Jacobian, change-of-variables factor, or integrability claim is introduced.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • PiLp.hasFDerivAt_ofLp
  • PiLp.hasFDerivAt_toLp
  • HasFDerivAt.comp
  • ContinuousLinearMap.comp_apply

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.