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

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

Read this first

Mathematical 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.\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Identify values in the open good set

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

  2. 2Transfer 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.

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.
  • 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 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_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.

Download module (.lean)
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)

Exact module and namespace context

Scope and omitted-condition boundaries
  • No differentiability on the box boundary is required.
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.