Coordinate partial derivatives on the edge-coupling space

First-order calculus for functions ρ : (Edge V → ℝ) → ℝ of the edge-coupling variables. Defines the coordinate update updateCoord, the coordinate basis directions edgeBasis, the single-coordinate partial derivative partialDeriv, iterated mixed partials along a list of edges (mixedPartialList), and the unordered forest mixed partial mixedPartial appearing in the integrand of the BKAR forest interpolation formula (see BKAR.Formula).

def BKAR.updateCoord {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) (t : ℝ) : Edge V → ℝ

Replace one BKAR edge coordinate in a parameter vector.

Equations

• BKAR.updateCoord x e t = Function.update x e t

@[simp]

theorem BKAR.updateCoord_self {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) (t : ℝ) : updateCoord x e t e = t

theorem BKAR.updateCoord_of_ne {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) {e e' : Edge V} (t : ℝ) (hne : e' ≠ e) : updateCoord x e t e' = x e'

@[simp]

theorem BKAR.updateCoord_same_value {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) : updateCoord x e (x e) = x

@[simp]

theorem BKAR.updateCoord_update_same {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) (s t : ℝ) : updateCoord (updateCoord x e s) e t = updateCoord x e t

def BKAR.edgeBasis {V : Type u_1} [DecidableEq V] (e : Edge V) : Edge V → ℝ

The coordinate basis vector for an edge.

Equations

• BKAR.edgeBasis e = Pi.single e 1

@[simp]

theorem BKAR.edgeBasis_self {V : Type u_1} [DecidableEq V] (e : Edge V) : edgeBasis e e = 1

theorem BKAR.edgeBasis_of_ne {V : Type u_1} [DecidableEq V] {e e' : Edge V} (hne : e' ≠ e) : edgeBasis e e' = 0

noncomputable def BKAR.partialDeriv {V : Type u_1} [DecidableEq V] (e : Edge V) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : ℝ

Partial derivative of ρ along one edge coordinate.

Equations

• BKAR.partialDeriv e ρ x = deriv (fun (t : ℝ) => ρ (BKAR.updateCoord x e t)) (x e)

theorem BKAR.partialDeriv_eq_deriv {V : Type u_1} [DecidableEq V] (e : Edge V) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : partialDeriv e ρ x = deriv (fun (t : ℝ) => ρ (updateCoord x e t)) (x e)

theorem BKAR.partialDeriv_updateCoord_self {V : Type u_1} [DecidableEq V] (e : Edge V) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) (s : ℝ) : partialDeriv e ρ (updateCoord x e s) = deriv (fun (t : ℝ) => ρ (updateCoord x e t)) s

theorem BKAR.partialDeriv_of_hasFDerivAt {V : Type u_1} [DecidableEq V] [Finite V] (e : Edge V) {ρ : (Edge V → ℝ) → ℝ} {x : Edge V → ℝ} {ρ' : (Edge V → ℝ) →L[ℝ] ℝ} (hρ : HasFDerivAt ρ ρ' x) : partialDeriv e ρ x = ρ' (edgeBasis e)

noncomputable def BKAR.mixedPartialList {V : Type u_1} [DecidableEq V] : List (Edge V) → ((Edge V → ℝ) → ℝ) → (Edge V → ℝ) → ℝ

Iterated mixed partial derivative along a list of edge coordinates.

Equations

• BKAR.mixedPartialList [] x✝ = x✝
• BKAR.mixedPartialList (e :: es) x✝ = BKAR.partialDeriv e (BKAR.mixedPartialList es x✝)

@[simp]

theorem BKAR.mixedPartialList_nil {V : Type u_1} [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) : mixedPartialList [] ρ = ρ

@[simp]

theorem BKAR.mixedPartialList_nil_apply {V : Type u_1} [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : mixedPartialList [] ρ x = ρ x

@[simp]

theorem BKAR.mixedPartialList_cons {V : Type u_1} [DecidableEq V] (e : Edge V) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : mixedPartialList (e :: es) ρ = partialDeriv e (mixedPartialList es ρ)

@[simp]

theorem BKAR.mixedPartialList_cons_apply {V : Type u_1} [DecidableEq V] (e : Edge V) (es : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : mixedPartialList (e :: es) ρ x = partialDeriv e (mixedPartialList es ρ) x

theorem BKAR.mixedPartialList_append {V : Type u_1} [DecidableEq V] (es₁ es₂ : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : mixedPartialList (es₁ ++ es₂) ρ = mixedPartialList es₁ (mixedPartialList es₂ ρ)

noncomputable def BKAR.Forest.mixedPartial {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) : (Edge V → ℝ) → ℝ

The mixed partial derivative indexed by the edge set of a forest.

Equations

• F.mixedPartial ρ = BKAR.mixedPartialList F.edges.toList ρ

theorem BKAR.Forest.mixedPartial_def {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) : F.mixedPartial ρ = mixedPartialList F.edges.toList ρ

theorem BKAR.Forest.mixedPartial_empty_edges {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.edges = ∅) (ρ : (Edge V → ℝ) → ℝ) : F.mixedPartial ρ = ρ

theorem BKAR.Forest.mixedPartial_empty_edges_apply {V : Type u_2} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.edges = ∅) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : F.mixedPartial ρ x = ρ x