Coordinate Gradient of the Two-Dimensional Product

Proved

ItoLemma.fin_two_coordinate_product_gradient_components

by WillR · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

coordinate-derivativeito-lemmaproduct-rulevector-ito

The partial derivatives of the product z₀z₁ are z₁ and z₀, represented by the coordinate-derivative operator used in the verified vector Itô formula. The derivative map is the one already established by the mission's Fréchet product derivative lemma.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_CoordDerivative
import Mathlib.Analysis.Calculus.FDeriv.Mul

Formal statement

theorem ItoLemma.fin_two_coordinate_product_gradient_components (z : Fin 2 → ℝ) :
    LevyStochCalc.coordDeriv
      (fun x : Fin 2 → ℝ =>
        x 0 • (ContinuousLinearMap.proj (1 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ) +
        x 1 • (ContinuousLinearMap.proj (0 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ))
      (0 : Fin 2) z = z 1 ∧
    LevyStochCalc.coordDeriv
      (fun x : Fin 2 → ℝ =>
        x 0 • (ContinuousLinearMap.proj (1 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ) +
        x 1 • (ContinuousLinearMap.proj (0 : Fin 2) : (Fin 2 → ℝ) →L[ℝ] ℝ))
      (1 : Fin 2) z = z 0 := by sorry

Source

Prove2Me coordinate derivative definition https://prove2.me/theorems/48f1793d-d529-4536-81b1-f98ae2c3d13d, inspected 26 October 2026; Mathlib Fréchet derivatives https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/FDeriv/Mul.html.

Human review

Endorsed by Shuze Chen · Oct 27, 2026
Confirmed by the moderator at approval.
Endorsed by WillR · Oct 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph