Active edges and one-edge forest extensions

The differential combinatorics of the forest induction. An edge of the complete graph is active for a forest F when its endpoints lie in different F-components, so that inserting it yields again a forest. Defines activeEdges, the insertion characterization of acyclicity, and the direction data activeDirection used by the one-edge expansion step of the BKAR forest interpolation formula (see BKAR.Formula).

noncomputable def BKAR.Forest.activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : Finset (Edge V)

Edges whose endpoints lie in different F-components.

Equations

• F.activeEdges = {e : BKAR.Edge V | ¬F.inSameComponent e.left e.right}

theorem BKAR.Forest.mem_activeEdges_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} : e ∈ F.activeEdges ↔ ¬F.inSameComponent e.left e.right

theorem BKAR.Forest.mem_activeEdges_of_not_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : ¬F.inSameComponent e.left e.right) : e ∈ F.activeEdges

theorem BKAR.Forest.not_inSameComponent_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.activeEdges) : ¬F.inSameComponent e.left e.right

theorem BKAR.Forest.empty_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] : (empty V).activeEdges = Finset.univ

noncomputable def BKAR.Forest.emptyActiveEdge {V : Type u_1} [Fintype V] [DecidableEq V] (e : Edge V) : ↥(empty V).activeEdges

View any edge as an active edge of the empty forest.

Equations

• BKAR.Forest.emptyActiveEdge e = ⟨e, ⋯⟩

@[simp]

theorem BKAR.Forest.emptyActiveEdge_val {V : Type u_1} [Fintype V] [DecidableEq V] (e : Edge V) : ↑(emptyActiveEdge e) = e

theorem BKAR.Forest.not_mem_edges_of_not_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : ¬F.inSameComponent e.left e.right) : e ∉ F.edges

theorem BKAR.Forest.not_mem_edges_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.activeEdges) : e ∉ F.edges

theorem BKAR.Forest.acyclic_insert_iff_edge {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∉ F.edges) : IsAcyclicEdgeSet (insert e F.edges) ↔ ¬F.inSameComponent e.left e.right

theorem BKAR.Forest.isAcyclicEdgeSet_insert_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.activeEdges) : IsAcyclicEdgeSet (insert e F.edges)

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

Direction in parameter space selected by the active edges of F.

Equations

• F.activeDirection = F.activeEdges.sum BKAR.edgeBasis

theorem BKAR.Forest.activeDirection_apply_of_mem {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.activeEdges) : F.activeDirection e = 1

theorem BKAR.Forest.activeDirection_apply_of_not_mem {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∉ F.activeEdges) : F.activeDirection e = 0

theorem BKAR.Forest.empty_activeDirection {V : Type u_1} [Fintype V] [DecidableEq V] : (empty V).activeDirection = oneConfig

theorem BKAR.Forest.interpWithFill_of_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) {e : Edge V} (he : F.inSameComponent e.left e.right) : F.interpWithFill u t e = F.pathMin u (F.pathInF e.left e.right he)

theorem BKAR.Forest.interpWithFill_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) {e : Edge V} (he : e ∈ F.activeEdges) : F.interpWithFill u t e = t

theorem BKAR.Forest.deriv_interpWithFill_apply_of_not_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : ¬F.inSameComponent e.left e.right) (t : ℝ) : deriv (fun (s : ℝ) => F.interpWithFill u s e) t = 1

theorem BKAR.Forest.deriv_interpWithFill_apply_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∈ F.activeEdges) (t : ℝ) : deriv (fun (s : ℝ) => F.interpWithFill u s e) t = 1

theorem BKAR.Forest.deriv_interpWithFill_apply_of_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : F.inSameComponent e.left e.right) (t : ℝ) : deriv (fun (s : ℝ) => F.interpWithFill u s e) t = 0

theorem BKAR.Forest.hasDerivAt_interpWithFill_apply_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∈ F.activeEdges) (t : ℝ) : HasDerivAt (fun (s : ℝ) => F.interpWithFill u s e) 1 t

theorem BKAR.Forest.hasDerivAt_interpWithFill_apply_of_not_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {e : Edge V} (he : e ∉ F.activeEdges) (t : ℝ) : HasDerivAt (fun (s : ℝ) => F.interpWithFill u s e) 0 t

theorem BKAR.Forest.hasDerivAt_interpWithFill {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) : HasDerivAt (fun (s : ℝ) => F.interpWithFill u s) F.activeDirection t

noncomputable def BKAR.Forest.activeEdgePartialSum {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : ℝ

Right-hand side of the differential identity.

Equations

• F.activeEdgePartialSum u ρ t = ∑ e ∈ F.activeEdges, BKAR.partialDeriv e ρ (F.interpWithFill u t)

theorem BKAR.Forest.activeEdgePartialSum_def {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : F.activeEdgePartialSum u ρ t = ∑ e ∈ F.activeEdges, partialDeriv e ρ (F.interpWithFill u t)

theorem BKAR.Forest.empty_activeEdgePartialSum {V : Type u_1} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : (empty V).activeEdgePartialSum u ρ t = ∑ e : Edge V, partialDeriv e ρ (constantConfig t)

def BKAR.Forest.ActiveEdgeDerivIdentityAt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : Prop

The proposition targeted by the chain-rule argument.

Equations

• F.ActiveEdgeDerivIdentityAt u ρ t = (deriv (fun (s : ℝ) => ρ (F.interpWithFill u s)) t = F.activeEdgePartialSum u ρ t)

theorem BKAR.Forest.activeEdgePartialSum_empty_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (hF : F.activeEdges = ∅) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) : F.activeEdgePartialSum u ρ t = 0

theorem BKAR.Forest.apply_activeDirection_eq_activeEdgePartialSum {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} {ρ' : (Edge V → ℝ) →L[ℝ] ℝ} (hρ : HasFDerivAt ρ ρ' (F.interpWithFill u t)) : ρ' F.activeDirection = F.activeEdgePartialSum u ρ t

theorem BKAR.Forest.hasDerivAt_rho_interpWithFill_of_hasFDerivAt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} {ρ' : (Edge V → ℝ) →L[ℝ] ℝ} (hρ : HasFDerivAt ρ ρ' (F.interpWithFill u t)) : HasDerivAt (fun (s : ℝ) => ρ (F.interpWithFill u s)) (F.activeEdgePartialSum u ρ t) t

theorem BKAR.Forest.hasDerivAt_rho_interpWithFill_of_differentiableAt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} (hρ : DifferentiableAt ℝ ρ (F.interpWithFill u t)) : HasDerivAt (fun (s : ℝ) => ρ (F.interpWithFill u s)) (F.activeEdgePartialSum u ρ t) t

theorem BKAR.Forest.differentialIdentityAt_of_hasFDerivAt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} {ρ' : (Edge V → ℝ) →L[ℝ] ℝ} (hρ : HasFDerivAt ρ ρ' (F.interpWithFill u t)) : F.ActiveEdgeDerivIdentityAt u ρ t

theorem BKAR.Forest.differentialIdentityAt_of_differentiableAt {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} (hρ : DifferentiableAt ℝ ρ (F.interpWithFill u t)) : F.ActiveEdgeDerivIdentityAt u ρ t

theorem BKAR.Forest.differentialIdentityAt_empty {V : Type u_1} [Fintype V] [DecidableEq V] (u : (empty V).EdgeParam → ℝ) {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} (hρ : DifferentiableAt ℝ ρ (constantConfig t)) : deriv (fun (s : ℝ) => ρ (constantConfig s)) t = ∑ e : Edge V, partialDeriv e ρ (constantConfig t)

theorem BKAR.Forest.differentialIdentityAt_emptyParam {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} {t : ℝ} (hρ : DifferentiableAt ℝ ρ (constantConfig t)) : deriv (fun (s : ℝ) => ρ (constantConfig s)) t = ∑ e : Edge V, partialDeriv e ρ (constantConfig t)