The one-edge expansion step

The fundamental-theorem-of-calculus step of the forest induction: for a one-edge extension of a forest, differentiating the interpolation family in the new edge parameter and integrating over [0, 1] splits a contribution into a boundary term and a contribution of the extended forest. Packages extensions along active edges as ActiveExtension and proves the derivative and integrability lemmas consumed by the recursion behind the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.EdgeExtension.mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) : e₀ ∈ F.activeEdges

The edge added by an extension is active for the old forest.

theorem BKAR.Forest.EdgeExtension.activeEdges_subset_erase {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) : F'.activeEdges ⊆ F.activeEdges.erase e₀

After a one-edge extension, every still-active edge was already active before, and the newly inserted edge is no longer active.

theorem BKAR.Forest.EdgeExtension.activeEdges_card_lt {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) : F'.activeEdges.card < F.activeEdges.card

A one-edge extension strictly decreases the number of active edges.

theorem BKAR.Forest.EdgeExtension.partialDeriv_interpWithFill_eq_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) {s : ℝ} (hu : ∀ (e : F.EdgeParam), s ≤ u e) : partialDeriv e₀ ρ (F.interpWithFill u s) = partialDeriv e₀ ρ (F'.interpWithFill (h.extendParam u s) s)

Pointwise re-interpretation of an active-edge integrand on a one-edge extension, under the ordered-simplex bound on the old parameters.

theorem BKAR.Forest.EdgeExtension.intervalIntegrable_partialDeriv_interpWithFill_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hbound : ∀ t ∈ Set.uIcc a b, ∀ (e : F.EdgeParam), t ≤ u e) (hint : IntervalIntegrable (fun (t : ℝ) => partialDeriv e₀ ρ (F.interpWithFill u t)) MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => partialDeriv e₀ ρ (F'.interpWithFill (h.extendParam u t) t)) MeasureTheory.volume a b

Interval integrability transfers across the one-edge extension re-interpretation.

theorem BKAR.Forest.EdgeExtension.integral_partialDeriv_interpWithFill_eq_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hbound : ∀ t ∈ Set.uIcc a b, ∀ (e : F.EdgeParam), t ≤ u e) : ∫ (t : ℝ) in a..b, partialDeriv e₀ ρ (F.interpWithFill u t) = ∫ (t : ℝ) in a..b, partialDeriv e₀ ρ (F'.interpWithFill (h.extendParam u t) t)

The one-edge summand in the differential identity may be integrated after reinterpreting its configuration on the extended forest.

theorem BKAR.Forest.EdgeExtension.mixedPartialList_cons_interpWithFill_eq_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) {s : ℝ} (hu : ∀ (e : F.EdgeParam), s ≤ u e) : partialDeriv e₀ (mixedPartialList es ρ) (F.interpWithFill u s) = mixedPartialList (e₀ :: es) ρ (F'.interpWithFill (h.extendParam u s) s)

Ordered-derivative form of the one-edge extension re-interpretation. The new edge is consed onto the explicit derivative list.

theorem BKAR.Forest.EdgeExtension.intervalIntegrable_mixedPartialList_cons_interpWithFill_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hbound : ∀ t ∈ Set.uIcc a b, ∀ (e : F.EdgeParam), t ≤ u e) (hint : IntervalIntegrable (fun (t : ℝ) => partialDeriv e₀ (mixedPartialList es ρ) (F.interpWithFill u t)) MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e₀ :: es) ρ (F'.interpWithFill (h.extendParam u t) t)) MeasureTheory.volume a b

Interval integrability transfers for the ordered-derivative form of the one-edge extension re-interpretation.

theorem BKAR.Forest.EdgeExtension.integral_partialDeriv_mixedPartialList_interpWithFill_eq_extension {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hbound : ∀ t ∈ Set.uIcc a b, ∀ (e : F.EdgeParam), t ≤ u e) : ∫ (t : ℝ) in a..b, partialDeriv e₀ (mixedPartialList es ρ) (F.interpWithFill u t) = ∫ (t : ℝ) in a..b, mixedPartialList (e₀ :: es) ρ (F'.interpWithFill (h.extendParam u t) t)

Integral congruence for the ordered-derivative form of the one-edge extension re-interpretation.

structure BKAR.Forest.ActiveExtension {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (e : Edge V) : Type u_1

A chosen one-edge forest extension for an edge.

• forest : Forest V

  The forest obtained by adjoining the selected active edge.

• extension : F.EdgeExtension self.forest e

theorem BKAR.Forest.ActiveExtension.mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) : e ∈ F.activeEdges

The edge of a chosen one-edge extension is active for the old forest.

theorem BKAR.Forest.ActiveExtension.activeEdges_card_lt {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) : h.forest.activeEdges.card < F.activeEdges.card

A chosen active extension strictly decreases the number of active edges.

theorem BKAR.Forest.edgeExtension_of_edges_eq_insert {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (he₀ : e₀ ∈ F.activeEdges) (hedges : F'.edges = insert e₀ F.edges) : F.EdgeExtension F' e₀

Any Forest representative whose edge set is obtained by inserting an active edge gives the corresponding one-edge extension certificate. Thus the hard existence problem for active extensions is exactly the construction of the inserted Forest representative.

def BKAR.Forest.activeExtensionOfEdgesEqInsert {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (he₀ : e₀ ∈ F.activeEdges) (hedges : F'.edges = insert e₀ F.edges) : F.ActiveExtension e₀

Packaging form of edgeExtension_of_edges_eq_insert: to produce an active extension, it is enough to produce a Forest representative with the inserted edge set.

Equations

• BKAR.Forest.activeExtensionOfEdgesEqInsert he₀ hedges = { forest := F', extension := ⋯ }

theorem BKAR.Forest.nonempty_activeExtension_of_exists_forest_edges_eq_insert {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e₀ : Edge V} (he₀ : e₀ ∈ F.activeEdges) (hforest : ∃ (F' : Forest V), F'.edges = insert e₀ F.edges) : Nonempty (F.ActiveExtension e₀)

Existential packaging form for the final choice-removal step. The remaining hard graph obligation is now isolated as existence of a Forest representative whose support is the inserted active edge set.

theorem BKAR.Forest.exists_forest_edges_eq_insert_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e₀ : Edge V} (he₀ : e₀ ∈ F.activeEdges) : ∃ (F' : Forest V), F'.edges = insert e₀ F.edges

theorem BKAR.Forest.nonempty_activeExtension_of_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e₀ : Edge V} (he₀ : e₀ ∈ F.activeEdges) : Nonempty (F.ActiveExtension e₀)

theorem BKAR.Forest.interpWithFill_eq_standardInterp_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (t : ℝ) (hF : F.activeEdges = ∅) : F.interpWithFill u t = F.standardInterp u

If no edge connects two different components, the fill-parameter interpolation has already reached the standard BKAR interpolation.

theorem BKAR.Forest.mixedPartialList_interpWithFill_eq_standardInterp_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (t : ℝ) (hF : F.activeEdges = ∅) : mixedPartialList es ρ (F.interpWithFill u t) = mixedPartialList es ρ (F.standardInterp u)

Terminal ordered-derivative form: with no active edges left, the interpolation parameter can be replaced by the standard configuration.

theorem BKAR.Forest.intervalIntegrable_activeEdgePartialSum {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => partialDeriv e ρ (F.interpWithFill u t)) MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => F.activeEdgePartialSum u ρ t) MeasureTheory.volume a b

The differential right-hand side is interval integrable once each active-edge partial derivative is interval integrable.

theorem BKAR.Forest.integral_activeEdgePartialSum_eq_sum_integrals {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => partialDeriv e ρ (F.interpWithFill u t)) MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, F.activeEdgePartialSum u ρ t = ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in a..b, partialDeriv e ρ (F.interpWithFill u t)

Split the integral of the differential right-hand side into the finite sum of one-edge integrals over the active edges of the forest.

theorem BKAR.Forest.integral_activeEdgePartialSum_eq_sub {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hρ : ∀ t ∈ Set.uIcc a b, DifferentiableAt ℝ ρ (F.interpWithFill u t)) (hint : IntervalIntegrable (fun (t : ℝ) => F.activeEdgePartialSum u ρ t) MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, F.activeEdgePartialSum u ρ t = ρ (F.interpWithFill u b) - ρ (F.interpWithFill u a)

Integrated form of the differential identity over one interpolation parameter. This is the analytic one-step expansion behind the ordered forest recursion.

theorem BKAR.Forest.sum_integrals_activeEdges_eq_sub {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hρ : ∀ t ∈ Set.uIcc a b, DifferentiableAt ℝ ρ (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => partialDeriv e ρ (F.interpWithFill u t)) MeasureTheory.volume a b) : ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in a..b, partialDeriv e ρ (F.interpWithFill u t) = ρ (F.interpWithFill u b) - ρ (F.interpWithFill u a)

Integrated differential identity after expanding the differential right-hand side as the active-edge sum.

theorem BKAR.Forest.rho_interpWithFill_eq_standardInterp_add_sum_integrals_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hρ : ∀ t ∈ Set.uIcc 0 b, DifferentiableAt ℝ ρ (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => partialDeriv e ρ (F.interpWithFill u t)) MeasureTheory.volume 0 b) : ρ (F.interpWithFill u b) = ρ (F.standardInterp u) + ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in 0..b, partialDeriv e ρ (F.interpWithFill u t)

Boundary-expansion form of the integrated differential identity, with the lower endpoint specialized to the standard interpolation configuration.

theorem BKAR.Forest.rho_oneConfig_eq_zeroConfig_add_sum_integrals_empty {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ ρ (constantConfig t)) (hint : ∀ (e : Edge V), IntervalIntegrable (fun (t : ℝ) => partialDeriv e ρ (constantConfig t)) MeasureTheory.volume 0 1) : ρ oneConfig = ρ zeroConfig + ∑ e : Edge V, ∫ (t : ℝ) in 0..1, partialDeriv e ρ (constantConfig t)

The true empty-start expansion: the first FTC step runs from the zero configuration to the all-one configuration and differentiates along every edge of the complete graph.

theorem BKAR.Forest.sum_integrals_activeEdges_mixedPartialList_eq_sub {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hρ : ∀ t ∈ Set.uIcc a b, DifferentiableAt ℝ (mixedPartialList es ρ) (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e :: es) ρ (F.interpWithFill u t)) MeasureTheory.volume a b) : ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in a..b, mixedPartialList (e :: es) ρ (F.interpWithFill u t) = mixedPartialList es ρ (F.interpWithFill u b) - mixedPartialList es ρ (F.interpWithFill u a)

Ordered-mixed-partial version of the integrated differential identity. This is the form used when the ordered recursion has already accumulated the derivative list es and expands by one active edge.

theorem BKAR.Forest.sum_integrals_activeEdges_mixedPartialList_eq_zero_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hF : F.activeEdges = ∅) : ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in a..b, mixedPartialList (e :: es) ρ (F.interpWithFill u t) = 0

The ordered active-edge integral remainder is zero when no active edges remain.

theorem BKAR.Forest.mixedPartialList_interpWithFill_eq_standardInterp_add_sum_integrals_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hρ : ∀ t ∈ Set.uIcc 0 b, DifferentiableAt ℝ (mixedPartialList es ρ) (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e :: es) ρ (F.interpWithFill u t)) MeasureTheory.volume 0 b) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in 0..b, mixedPartialList (e :: es) ρ (F.interpWithFill u t)

Boundary-expansion form of the ordered-mixed-partial differential identity. This is the local recursion formula before the active-edge summands are reinterpreted as one-edge forest extensions.

theorem BKAR.Forest.mixedPartial_eq_standard_add_integralSum_activeEdges_of_emptyActiveEdges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hF : F.activeEdges = ∅) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in 0..b, mixedPartialList (e :: es) ρ (F.interpWithFill u t)

Terminal form of the ordered-recursion step: with no active edges, the boundary term is the whole contribution and the next remainder is zero.

theorem BKAR.Forest.sum_integrals_activeEdges_eq_sum_activeExtensions {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (a b : ℝ) (hbound : ∀ t ∈ Set.uIcc a b, ∀ (e : F.EdgeParam), t ≤ u e) (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) : ∑ e ∈ F.activeEdges, ∫ (t : ℝ) in a..b, mixedPartialList (e :: es) ρ (F.interpWithFill u t) = ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in a..b, mixedPartialList (↑e :: es) ρ ((extensions e).forest.interpWithFill (⋯.extendParam u t) t)

Rewrite the active-edge remainder as a sum over explicitly chosen one-edge forest extensions.

theorem BKAR.Forest.mixedPartialList_interpWithFill_eq_standardInterp_add_sum_activeExtensions {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (es : List (Edge V)) (u : F.EdgeParam → ℝ) (ρ : (Edge V → ℝ) → ℝ) (b : ℝ) (hbound : ∀ t ∈ Set.uIcc 0 b, ∀ (e : F.EdgeParam), t ≤ u e) (hρ : ∀ t ∈ Set.uIcc 0 b, DifferentiableAt ℝ (mixedPartialList es ρ) (F.interpWithFill u t)) (hint : ∀ e ∈ F.activeEdges, IntervalIntegrable (fun (t : ℝ) => mixedPartialList (e :: es) ρ (F.interpWithFill u t)) MeasureTheory.volume 0 b) (extensions : (e : ↥F.activeEdges) → F.ActiveExtension ↑e) : mixedPartialList es ρ (F.interpWithFill u b) = mixedPartialList es ρ (F.standardInterp u) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..b, mixedPartialList (↑e :: es) ρ ((extensions e).forest.interpWithFill (⋯.extendParam u t) t)

Boundary-expansion form whose active-edge remainder has already been reinterpreted as a sum over explicitly chosen one-edge forest extensions.