LeanPool.DirectedTopologyLean4.Interpolate

theorem interp_mem_I (T a b : ↑unitInterval) : ↑(unitInterval.symm T) * ↑a + ↑T * ↑b ∈ unitInterval

theorem interp_left_mem_I (T a : ↑unitInterval) : ↑(unitInterval.symm T) * ↑a + ↑T ∈ unitInterval

theorem interp_right_mem_I (T b : ↑unitInterval) : ↑(unitInterval.symm T) + ↑T * ↑b ∈ unitInterval

theorem interp_const_le_of_le_of_le {a b T₀ T₁ : ↑unitInterval} (hab : a ≤ b) (hT : T₀ ≤ T₁) : ↑(unitInterval.symm T₀) * ↑a + ↑T₀ * ↑b ≤ ↑(unitInterval.symm T₁) * ↑a + ↑T₁ * ↑b

def interpolateConst (a b : ↑unitInterval) : C(↑unitInterval, ↑unitInterval)

The continuous map t ↦ (1 - t) * a + t * b interpolating between a and b in I.

Equations

• interpolateConst a b = { toFun := fun (t : ↑unitInterval) => ⟨↑(unitInterval.symm t) * ↑a + ↑t * ↑b, ⋯⟩, continuous_toFun := ⋯ }

def directedInterpolateConst {a b : ↑unitInterval} (h : a ≤ b) : D(↑unitInterval,↑unitInterval)

The directed-map version of interpolateConst when a ≤ b.

Equations

• directedInterpolateConst h = { toContinuousMap := interpolateConst a b, directed_toFun := ⋯ }

def interpolate (f g : C(↑unitInterval, ↑unitInterval)) : C(↑unitInterval × ↑unitInterval, ↑unitInterval)

Two-parameter interpolation (s, t) ↦ (1 - s) * f t + s * g t.

Equations

• interpolate f g = { toFun := fun (t : ↑unitInterval × ↑unitInterval) => ⟨↑(unitInterval.symm t.1) * ↑(f t.2) + ↑t.1 * ↑(g t.2), ⋯⟩, continuous_toFun := ⋯ }

theorem interpolate_left (f g : C(↑unitInterval, ↑unitInterval)) : (interpolate f g).curry 0 = f

theorem interpolate_right (f g : C(↑unitInterval, ↑unitInterval)) : (interpolate f g).curry 1 = g

theorem interpolate_constant_apply (f g : C(↑unitInterval, ↑unitInterval)) (t v : ↑unitInterval) (hf : f t = v) (hg : g t = v) (x : ↑unitInterval) : (interpolate f g) (x, t) = v

theorem directed_interpolate (f g : D(↑unitInterval,↑unitInterval)) (h : ∀ (t : ↑unitInterval), f t ≤ g t) : DirectedMap.Directed (interpolate f.toContinuousMap g.toContinuousMap)