The Dirichlet solution operator on continuous acceleration paths.

@[reducible, inline]

abbrev PlanarMidpoint.UnitInterval : Set ℝ

The compact real parameter interval [0, 1].

Equations

• PlanarMidpoint.UnitInterval = Set.Icc 0 1

@[reducible, inline]

abbrev PlanarMidpoint.AccelerationPath : Type

Continuous planar acceleration paths on the unit interval.

Equations

• PlanarMidpoint.AccelerationPath = C(↑PlanarMidpoint.UnitInterval, PlanarMidpoint.E)

@[reducible, inline]

abbrev PlanarMidpoint.PhasePath : Type

Continuous position-velocity paths on the unit interval.

Equations

• PlanarMidpoint.PhasePath = C(↑PlanarMidpoint.UnitInterval, PlanarMidpoint.E × PlanarMidpoint.E)

noncomputable def PlanarMidpoint.pathExtend (f : AccelerationPath) (t : ℝ) : E

Extension of an acceleration path by clamping the parameter to the unit interval.

Equations

• PlanarMidpoint.pathExtend f t = f (Set.projIcc 0 1 PlanarMidpoint.pathExtend._proof_1 t)

theorem PlanarMidpoint.continuous_pathExtend (f : AccelerationPath) : Continuous (pathExtend f)

theorem PlanarMidpoint.pathExtend_mem (f : AccelerationPath) (t : ℝ) (ht : t ∈ UnitInterval) : pathExtend f t = f ⟨t, ht⟩

noncomputable def PlanarMidpoint.pathPrimitive (f : AccelerationPath) (t : ℝ) : E

The integral of an extended acceleration path from zero to the given time.

Equations

• PlanarMidpoint.pathPrimitive f t = ∫ (s : ℝ) in 0..t, PlanarMidpoint.pathExtend f s

theorem PlanarMidpoint.hasDerivAt_pathPrimitive (f : AccelerationPath) (t : ℝ) : HasDerivAt (pathPrimitive f) (pathExtend f t) t

theorem PlanarMidpoint.continuous_pathPrimitive (f : AccelerationPath) : Continuous (pathPrimitive f)

noncomputable def PlanarMidpoint.pathSecondPrimitive (f : AccelerationPath) (t : ℝ) : E

The second primitive of an extended acceleration path.

Equations

• PlanarMidpoint.pathSecondPrimitive f t = ∫ (s : ℝ) in 0..t, PlanarMidpoint.pathPrimitive f s

theorem PlanarMidpoint.hasDerivAt_pathSecondPrimitive (f : AccelerationPath) (t : ℝ) : HasDerivAt (pathSecondPrimitive f) (pathPrimitive f t) t

noncomputable def PlanarMidpoint.greenPosition (f : AccelerationPath) (t : ℝ) : E

The second primitive with its endpoint chord removed.

Equations

• PlanarMidpoint.greenPosition f t = PlanarMidpoint.pathSecondPrimitive f t - t • PlanarMidpoint.pathSecondPrimitive f 1

noncomputable def PlanarMidpoint.greenVelocity (f : AccelerationPath) (t : ℝ) : E

The first primitive minus the endpoint correction.

Equations

• PlanarMidpoint.greenVelocity f t = PlanarMidpoint.pathPrimitive f t - PlanarMidpoint.pathSecondPrimitive f 1

theorem PlanarMidpoint.hasDerivAt_greenPosition (f : AccelerationPath) (t : ℝ) : HasDerivAt (greenPosition f) (greenVelocity f t) t

theorem PlanarMidpoint.hasDerivAt_greenVelocity (f : AccelerationPath) (t : ℝ) : HasDerivAt (greenVelocity f) (pathExtend f t) t

@[simp]

theorem PlanarMidpoint.greenPosition_zero (f : AccelerationPath) : greenPosition f 0 = 0

@[simp]

theorem PlanarMidpoint.greenPosition_one (f : AccelerationPath) : greenPosition f 1 = 0

noncomputable def PlanarMidpoint.greenPath (f : AccelerationPath) : PhasePath

The position-velocity path solving the zero-endpoint Dirichlet problem.

Equations

• PlanarMidpoint.greenPath f = { toFun := fun (t : ↑PlanarMidpoint.UnitInterval) => (PlanarMidpoint.greenPosition f ↑t, PlanarMidpoint.greenVelocity f ↑t), continuous_toFun := ⋯ }

theorem PlanarMidpoint.norm_greenPath_le (f : AccelerationPath) : ‖greenPath f‖ ≤ ‖f‖

theorem PlanarMidpoint.pathPrimitive_add (f g : AccelerationPath) (t : ℝ) : pathPrimitive (f + g) t = pathPrimitive f t + pathPrimitive g t

theorem PlanarMidpoint.pathPrimitive_smul (r : ℝ) (f : AccelerationPath) (t : ℝ) : pathPrimitive (r • f) t = r • pathPrimitive f t

theorem PlanarMidpoint.pathSecondPrimitive_add (f g : AccelerationPath) (t : ℝ) : pathSecondPrimitive (f + g) t = pathSecondPrimitive f t + pathSecondPrimitive g t

theorem PlanarMidpoint.pathSecondPrimitive_smul (r : ℝ) (f : AccelerationPath) (t : ℝ) : pathSecondPrimitive (r • f) t = r • pathSecondPrimitive f t

noncomputable def PlanarMidpoint.greenLinear : AccelerationPath →ₗ[ℝ] PhasePath

Linearity of the Dirichlet Green construction on continuous acceleration paths.

Equations

• PlanarMidpoint.greenLinear = { toFun := PlanarMidpoint.greenPath, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def PlanarMidpoint.greenOperator : AccelerationPath →L[ℝ] PhasePath

The bounded Dirichlet Green operator, with operator norm at most one.

Equations

• PlanarMidpoint.greenOperator = PlanarMidpoint.greenLinear.mkContinuous 1 ⋯

@[simp]

theorem PlanarMidpoint.greenOperator_apply (f : AccelerationPath) (t : ↑UnitInterval) : (greenOperator f) t = (greenPosition f ↑t, greenVelocity f ↑t)

theorem PlanarMidpoint.norm_greenOperator_le : ‖greenOperator‖ ≤ 1