Symmetry of mixed partial derivatives

Under the global smoothness hypothesis BKARContDiff, coordinate partial derivatives on the edge-coupling space commute. Consequently mixedPartialList is invariant under permutations of its edge list and, for any enumeration of a forest's edge set, agrees with the unordered forest mixed partial mixedPartial. This order-independence is what lets the order-by-order expansion be regrouped into the order-free integrand of the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.BKARContDiff.partialDeriv_comm_apply {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (e f : Edge V) (x : Edge V → ℝ) : BKAR.partialDeriv e (BKAR.partialDeriv f ρ) x = BKAR.partialDeriv f (BKAR.partialDeriv e ρ) x

Under the global BKAR smoothness hypothesis, coordinate partial derivatives commute pointwise. This is the analytic order-independence ingredient needed to replace recursive ordered-sector mixed partials by the order-free forest mixed partial.

theorem BKAR.BKARContDiff.partialDeriv_comm {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (e f : Edge V) : BKAR.partialDeriv e (BKAR.partialDeriv f ρ) = BKAR.partialDeriv f (BKAR.partialDeriv e ρ)

theorem BKAR.BKARContDiff.mixedPartialList_cons_cons_comm {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (e f : Edge V) (es : List (Edge V)) : BKAR.mixedPartialList (e :: f :: es) ρ = BKAR.mixedPartialList (f :: e :: es) ρ

theorem BKAR.BKARContDiff.mixedPartialList_eq_of_perm {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} {es₁ es₂ : List (Edge V)} (hperm : es₁.Perm es₂) (hρ : BKARContDiff ρ) : BKAR.mixedPartialList es₁ ρ = BKAR.mixedPartialList es₂ ρ

Mixed partials along two permuted edge lists agree under BKARContDiff. This is the global analytic bridge from canonical-order expressions to the unordered forest-edge derivative in the final cube contribution.

theorem BKAR.Forest.mixedPartial_eq_mixedPartialList_of_mem_edgeOrders {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {ρ : (Edge V → ℝ) → ℝ} {order : List (Edge V)} (horder : order ∈ F.edgeOrders) (hρ : BKARContDiff ρ) : F.mixedPartial ρ = mixedPartialList order.reverse ρ