The global smoothness hypothesis

Defines BKARContDiff ρ, the hypothesis that ρ is C^∞ (ContDiff ℝ (∞ : WithTop ℕ∞)) on the finite edge-coupling space, and derives from it the analytic facts consumed by the proof of the BKAR forest interpolation formula (see BKAR.Formula): continuity and differentiability of iterated mixed partials, and integrability of the integrands appearing in the induction.

The classical formula requires only finitely many derivatives (C^{|V|-1} suffices); assuming C^∞ is a deliberate strengthening of the hypothesis that keeps the analytic bookkeeping uniform in the induction.

def BKAR.BKARContDiff {V : Type u_1} [Fintype V] (ρ : (Edge V → ℝ) → ℝ) : Prop

The global smoothness hypothesis intended to discharge the analytic side conditions in the BKAR induction.

It is deliberately only C^∞ smoothness on the finite edge-parameter space; the order/support conditions remain separate combinatorial obligations.

Equations

• BKAR.BKARContDiff ρ = ContDiff ℝ (↑⊤) ρ

theorem BKAR.BKARContDiff.contDiff {V : Type u_1} [Fintype V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) : ContDiff ℝ (↑⊤) ρ

theorem BKAR.BKARContDiff.continuous {V : Type u_1} [Fintype V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) : Continuous ρ

theorem BKAR.BKARContDiff.differentiable {V : Type u_1} [Fintype V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) : Differentiable ℝ ρ

theorem BKAR.BKARContDiff.differentiableAt {V : Type u_1} [Fintype V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (x : Edge V → ℝ) : DifferentiableAt ℝ ρ x

theorem BKAR.BKARContDiff.fderiv_contDiff {V : Type u_1} [Fintype V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) : ContDiff ℝ (↑⊤) (fderiv ℝ ρ)

theorem BKAR.BKARContDiff.fderiv_apply_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (e : Edge V) : ContDiff ℝ ↑⊤ fun (x : Edge V → ℝ) => (fderiv ℝ ρ x) (edgeBasis e)

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

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

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

theorem BKAR.BKARContDiff.mixedPartialList_differentiableAt {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) (x : Edge V → ℝ) : DifferentiableAt ℝ (BKAR.mixedPartialList es ρ) x

theorem BKAR.BKARContDiff.mixedPartialList_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) {γ : ℝ → Edge V → ℝ} (hγ : Continuous γ) : Continuous fun (t : ℝ) => BKAR.mixedPartialList es ρ (γ t)

theorem BKAR.BKARContDiff.mixedPartialList_intervalIntegrable_comp {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) {γ : ℝ → Edge V → ℝ} (hγ : Continuous γ) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList es ρ (γ t)) MeasureTheory.volume a b

theorem BKAR.intervalIntegral_continuous_primitive_of_continuous {f : ℝ → ℝ} (hf : Continuous f) (a : ℝ) : Continuous fun (b : ℝ) => ∫ (t : ℝ) in a..b, f t

A continuous one-dimensional integrand has a continuous moving-upper-bound primitive.

theorem BKAR.intervalIntegral_primitive_intervalIntegrable_of_continuous {f : ℝ → ℝ} (hf : Continuous f) (a b c : ℝ) : IntervalIntegrable (fun (x : ℝ) => ∫ (t : ℝ) in a..x, f t) MeasureTheory.volume b c

The moving-upper-bound primitive of a continuous one-dimensional integrand is integrable.

theorem BKAR.intervalIntegral_primitive_intervalIntegrable_of_intervalIntegrable {f : ℝ → ℝ} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) : IntervalIntegrable (fun (x : ℝ) => ∫ (t : ℝ) in a..x, f t) MeasureTheory.volume a b

If an integrand is interval-integrable on [a, b], then its moving primitive from a is interval-integrable on the same interval.

def BKAR.ListPathContinuous {X : Type u_2} [TopologicalSpace X] (n : ℕ) (tsPath : X → List ℝ) : Prop

A path of finite parameter lists with fixed length whose coordinates are all continuous. This is the small API needed for recursive ordered-simplex diagonals such as prefixTs ++ [t₁] ++ [t₂].

Equations

• BKAR.ListPathContinuous n tsPath = ((∀ (x : X), (tsPath x).length = n) ∧ ∀ (i : ℕ), Continuous fun (x : X) => (tsPath x).getD i 0)

theorem BKAR.ListPathContinuous.const {X : Type u_2} [TopologicalSpace X] (ts : List ℝ) : ListPathContinuous ts.length fun (x : X) => ts

theorem BKAR.ListPathContinuous.comp {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {tsPath : X → List ℝ} (hts : ListPathContinuous n tsPath) {f : Y → X} (hf : Continuous f) : ListPathContinuous n fun (y : Y) => tsPath (f y)

theorem BKAR.ListPathContinuous.append_singleton {X : Type u_2} [TopologicalSpace X] {n : ℕ} {tsPath : X → List ℝ} (hts : ListPathContinuous n tsPath) {tPath : X → ℝ} (ht : Continuous tPath) : ListPathContinuous (n + 1) fun (x : X) => tsPath x ++ [tPath x]

theorem BKAR.constantConfig_contDiff {V : Type u_1} [Fintype V] : ContDiff ℝ (↑⊤) constantConfig

theorem BKAR.constantConfig_continuous {V : Type u_1} [Finite V] : Continuous constantConfig

theorem BKAR.updateCoord_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) : ContDiff ℝ (↑⊤) (updateCoord x e)

theorem BKAR.Forest.EdgeExtension.extendParam_continuous {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} (h : F.EdgeExtension F' e) (u : F.EdgeParam → ℝ) : Continuous fun (t : ℝ) => h.extendParam u t

theorem BKAR.Forest.EdgeExtension.extendParam_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e : Edge V} {X : Type u_2} [TopologicalSpace X] (h : F.EdgeExtension F' e) {uPath : X → F.EdgeParam → ℝ} (hu : Continuous uPath) {tPath : X → ℝ} (ht : Continuous tPath) : Continuous fun (x : X) => h.extendParam (uPath x) (tPath x)

theorem BKAR.Forest.interpWithFill_contDiff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : ContDiff ℝ (↑⊤) (F.interpWithFill u)

theorem BKAR.Forest.interpWithFill_continuous {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (u : F.EdgeParam → ℝ) : Continuous (F.interpWithFill u)

theorem BKAR.Forest.paramValue_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {X : Type u_2} [TopologicalSpace X] {uPath : X → F.EdgeParam → ℝ} (hu : Continuous uPath) (e : Edge V) : Continuous fun (x : X) => F.paramValue (uPath x) e

theorem BKAR.Forest.pathMinAux_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {X : Type u_2} [TopologicalSpace X] {uPath : X → F.EdgeParam → ℝ} (hu : Continuous uPath) {aPath : X → ℝ} (ha : Continuous aPath) (γ : List (Edge V)) : Continuous fun (x : X) => F.pathMinAux (uPath x) (aPath x) γ

theorem BKAR.Forest.pathMin_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {X : Type u_2} [TopologicalSpace X] {uPath : X → F.EdgeParam → ℝ} (hu : Continuous uPath) (γ : List (Edge V)) : Continuous fun (x : X) => F.pathMin (uPath x) γ

theorem BKAR.Forest.standardInterp_continuous_comp {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {X : Type u_2} [TopologicalSpace X] {uPath : X → F.EdgeParam → ℝ} (hu : Continuous uPath) : Continuous fun (x : X) => F.standardInterp (uPath x)

theorem BKAR.BKARContDiff.comp_updateCoord {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (x : Edge V → ℝ) (e : Edge V) : ContDiff ℝ ↑⊤ fun (t : ℝ) => ρ (updateCoord x e t)

theorem BKAR.BKARContDiff.continuous_comp_updateCoord {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (x : Edge V → ℝ) (e : Edge V) : Continuous fun (t : ℝ) => ρ (updateCoord x e t)

theorem BKAR.BKARContDiff.intervalIntegrable_comp_updateCoord {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (x : Edge V → ℝ) (e : Edge V) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => ρ (updateCoord x e t)) MeasureTheory.volume a b

theorem BKAR.BKARContDiff.mixedPartialList_interpWithFill_continuous {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) (F : Forest V) (u : F.EdgeParam → ℝ) : Continuous fun (t : ℝ) => BKAR.mixedPartialList es ρ (F.interpWithFill u t)

theorem BKAR.BKARContDiff.mixedPartialList_interpWithFill_intervalIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) (F : Forest V) (u : F.EdgeParam → ℝ) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList es ρ (F.interpWithFill u t)) MeasureTheory.volume a b

theorem BKAR.BKARContDiff.mixedPartialList_standardInterp_intervalIntegrable {V : Type u_1} [Fintype V] [DecidableEq V] {ρ : (Edge V → ℝ) → ℝ} (hρ : BKARContDiff ρ) (es : List (Edge V)) (F : Forest V) {uPath : ℝ → F.EdgeParam → ℝ} (hu : Continuous uPath) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => BKAR.mixedPartialList es ρ (F.standardInterp (uPath t))) MeasureTheory.volume a b