Actual profile normalization of continuous time paths

A positive scalar time profile gives inverse bounded linear scaling maps. The norm of a normalized path is bounded directly by its profile estimate; no quotient of the maximum and minimum profile enters that estimate.

noncomputable def EulerContinuousTimeWeight.weight {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) : C(K, E) →L[ℝ] C(K, E)

Multiplication by the literal scalar profile.

Equations

• EulerContinuousTimeWeight.weight g = EulerContinuousTimeIntegral.multiplier { toFun := fun (t : K) => g t • ContinuousLinearMap.id ℝ E, continuous_toFun := ⋯ }

@[simp]

theorem EulerContinuousTimeWeight.weight_apply {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (f : C(K, E)) (t : K) : ((weight g) f) t = g t • f t

noncomputable def EulerContinuousTimeWeight.reciprocal {K : Type u_1} [TopologicalSpace K] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) : C(K, ℝ)

The reciprocal of a positive continuous profile is an actual continuous path.

Equations

• EulerContinuousTimeWeight.reciprocal g hg = { toFun := fun (t : K) => (g t)⁻¹, continuous_toFun := ⋯ }

noncomputable def EulerContinuousTimeWeight.normalize {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) : C(K, E) →L[ℝ] C(K, E)

Profile division as a genuine bounded linear map.

Equations

• EulerContinuousTimeWeight.normalize g hg = EulerContinuousTimeWeight.weight (EulerContinuousTimeWeight.reciprocal g hg)

@[simp]

theorem EulerContinuousTimeWeight.normalize_apply {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (f : C(K, E)) (t : K) : ((normalize g hg) f) t = (g t)⁻¹ • f t

theorem EulerContinuousTimeWeight.normalize_weight {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (f : C(K, E)) : (normalize g hg) ((weight g) f) = f

Weighting and normalization are actual inverse operators.

theorem EulerContinuousTimeWeight.weight_normalize {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (f : C(K, E)) : (weight g) ((normalize g hg) f) = f

Normalization and weighting are inverse in the other order too.

theorem EulerContinuousTimeWeight.weight_pointwise_bound {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 ≤ g t) (f : C(K, E)) (t : K) : ‖((weight g) f) t‖ ≤ g t * ‖f‖

Literal pointwise control of a weighted path, with no profile extremum.

theorem EulerContinuousTimeWeight.normalize_norm_le {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (f : C(K, E)) (D : ℝ) (hD : 0 ≤ D) (hf : ∀ (t : K), ‖f t‖ ≤ D * g t) : ‖(normalize g hg) f‖ ≤ D

A pointwise profile bound gives the normalized uniform norm directly.

theorem EulerContinuousTimeWeight.normalize_multiplier {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (A : C(K, E →L[ℝ] E)) (f : C(K, E)) : (normalize g hg) ((EulerContinuousTimeIntegral.multiplier A) f) = (EulerContinuousTimeIntegral.multiplier A) ((normalize g hg) f)

Scalar normalization commutes with every coefficient multiplier.

theorem EulerContinuousTimeWeight.weight_multiplier {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (A : C(K, E →L[ℝ] E)) (f : C(K, E)) : (weight g) ((EulerContinuousTimeIntegral.multiplier A) f) = (EulerContinuousTimeIntegral.multiplier A) ((weight g) f)

Scalar weighting commutes with every coefficient multiplier.