ASTIS mathematical exposition

Apply the product derivative on a common exceptional-set complement

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

Statement

For endpoints a,b, arbitrary s⊆P, and fields χ,G,ℓ,B, suppose χ has derivative ℓ(x) and G has derivative B(x) at every x∈O∖s. Then χG has derivative M(x)=χ(x)B(x)+ℓ(x).smulRight(G(x)) at every such x.

\[D\chi=\ell,\ DG=B\text{ on }O\setminus s\quad\Longrightarrow\quad D(\chi G)=M\text{ on }O\setminus s.\]

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.
χ: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.
s⊆P is arbitrary: despite the declaration name, no `s.Countable` hypothesis is present.
For each x∈O∖s, HasFDerivAt χ (ℓ x) x and HasFDerivAt G (B x) x. No a≤b or closed-box continuity premise.

Mathematical proof

1. Fix an allowed point and use both derivative witnesses

For x∈O∖s, the two hypotheses give actual derivatives at that same x. Apply the pointwise scalar-vector product rule there; x was arbitrary in the good set.

\[x\in O\setminus s\Longrightarrow D(\chi G)(x)[v]=\chi(x)B(x)[v]+\ell(x)[v]G(x).\]

Corresponding Lean step

hasFDerivAt_smul_vectorField_of_hasFDerivAt χ (χ' x) G (G' x) x (hχ x hx) (hG x hx).

Lean statement · hasFDerivAt_smul_vectorField_off_countable

This is a pointwise quantification wrapper. Countability is not used until a later theorem wants to ignore s in a Lebesgue-a.e. argument.

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 hasFDerivAt_smul_vectorField_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (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) → ℝ))
    (hχ : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hG : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x) :
    ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt (fun y => χ y • G y)
        (χ x • G' x + (χ' x).smulRight (G x)) x

Exact module and namespace context

Lean proof · hasFDerivAt_smul_vectorField_off_countable

For x∈O∖s, the two hypotheses give actual derivatives at that same x. Apply the pointwise scalar-vector product rule there; x was arbitrary in the good set. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem hasFDerivAt_smul_vectorField_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (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) → ℝ))
    (hχ : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hG : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x) :
    ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt (fun y => χ y • G y)
        (χ x • G' x + (χ' x).smulRight (G x)) x := by
  intro x hx
  exact hasFDerivAt_smul_vectorField_of_hasFDerivAt χ (χ' x) G (G' x) x
    (hχ x hx) (hG x hx)

/-- Closed-box continuity of the cutoff-smul product-rule trace from only the
coordinate component continuity needed by the trace summand.

The expanded summand is
`χ x * (G' x eᵢ)ᵢ + (χ' x eᵢ) * (G x)ᵢ`.  This leaf therefore assumes
continuity of exactly these component functions.  It does not prove that `χ'`
or `G'` are derivative fields, does not construct cutoffs, and does not prove
boundary cancellation or weighted integration by parts. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not silently add s.Countable to this statement, or infer an a.e. result for arbitrary s.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.hasFDerivAt_smul_vectorField_of_hasFDerivAt

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS 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.hasFDerivAt_smul_vectorField_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.

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