Actual finite weighted forcing norms in the Bochner time space.

Actual L²-time convergence of finite Hilbert forcing norms.

def EulerFamilyNormTime.familyHilbertMap {I : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] : (I → H) →L[ℝ] PiLp 2 fun (x : I) => H

The ordinary finite family as its genuine Hilbert-sum norm model.

Equations

• EulerFamilyNormTime.familyHilbertMap = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : I) => H).symm

theorem EulerFamilyNormTime.familyNorm_eq_piLp {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (u : I → H) : EulerFiniteMetricEnergy.familyNorm u = ‖familyHilbertMap u‖

The actual root of the sum of squares equals the genuine finite L²-product norm.

theorem EulerFamilyNormTime.familyNorm_lipschitz {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] : LipschitzWith ‖familyHilbertMap‖₊ EulerFiniteMetricEnergy.familyNorm

The finite forcing norm is Lipschitz, with a fixed base-cardinality constant.

noncomputable def EulerFamilyNormTime.familyNormTime {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T (I → H))) : ↥(EulerTimeLp.TimeLp T ℝ)

The actual scalar finite-family norm represented in Bochner L² time.

Equations

• EulerFamilyNormTime.familyNormTime T u = ⋯.compLp ⋯ u

theorem EulerFamilyNormTime.familyNormTime_ae {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T (I → H))) : ↑↑(familyNormTime T u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => EulerFiniteMetricEnergy.familyNorm (↑↑u t)

This scalar Bochner element is the literal family forcing norm almost everywhere.

theorem EulerFamilyNormTime.familyNormTime_tendsto {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (u : ℕ → ↥(EulerTimeLp.TimeLp T (I → H))) (v : ↥(EulerTimeLp.TimeLp T (I → H))) (hu : Filter.Tendsto u Filter.atTop (nhds v)) : Filter.Tendsto (fun (n : ℕ) => familyNormTime T (u n)) Filter.atTop (nhds (familyNormTime T v))

Strong L²-time forcing convergence gives strong convergence of its actual finite-family norm.

theorem EulerFamilyNormTime.integral_familyNorm_tendsto {I : Type u_1} {H : Type u_2} [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (a : ↥(EulerTimeLp.TimeLp T ℝ)) (u : ℕ → ↥(EulerTimeLp.TimeLp T (I → H))) (v : ↥(EulerTimeLp.TimeLp T (I → H))) (hu : Filter.Tendsto u Filter.atTop (nhds v)) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ), ↑↑a t * EulerFiniteMetricEnergy.familyNorm (↑↑(u n) t) ∂EulerTimeLp.timeMeasure T) Filter.atTop (nhds (∫ (t : ℝ), ↑↑a t * EulerFiniteMetricEnergy.familyNorm (↑↑v t) ∂EulerTimeLp.timeMeasure T))

Weighted time integrals of actual family forcing norms pass through strong L² approximations.

noncomputable def EulerWeightedForcingTime.scalarTimeMultiplier (T : ℝ) (hT : 0 ≤ T) (w : C(↑(Set.Icc 0 T), ℝ)) : ↥(EulerTimeLp.TimeLp T ℝ) →L[ℝ] ↥(EulerTimeLp.TimeLp T ℝ)

Multiplication by a continuous scalar time weight as a genuine Bochner operator.

Equations

• EulerWeightedForcingTime.scalarTimeMultiplier T hT w = EulerTimeLp.timeMultiplier T hT { toFun := fun (t : ↑(Set.Icc 0 T)) => w t • ContinuousLinearMap.id ℝ ℝ, continuous_toFun := ⋯ }

theorem EulerWeightedForcingTime.scalarTimeMultiplier_ae (T : ℝ) (hT : 0 ≤ T) (w : C(↑(Set.Icc 0 T), ℝ)) (u : ↥(EulerTimeLp.TimeLp T ℝ)) : ↑↑((scalarTimeMultiplier T hT w) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => EulerVolterraConvolution.extendPath T hT w t * ↑↑u t

The actual scalar multiplier has its literal weighted representative.

noncomputable def EulerWeightedForcingTime.weightedForcingTime {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (hT : 0 ≤ T) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → ↥(EulerTimeLp.TimeLp T (I → H))) : ↥(EulerTimeLp.TimeLp T ℝ)

The genuine finite weighted sum of actual forcing norms represented in L² time.

Equations

• EulerWeightedForcingTime.weightedForcingTime T hT w F = ∑ i : A, (EulerWeightedForcingTime.scalarTimeMultiplier T hT (w i)) (EulerFamilyNormTime.familyNormTime T (F i))

theorem EulerWeightedForcingTime.weightedForcingTime_ae {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (hT : 0 ≤ T) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → ↥(EulerTimeLp.TimeLp T (I → H))) : ↑↑(weightedForcingTime T hT w F) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => ∑ i : A, EulerVolterraConvolution.extendPath T hT (w i) t * EulerFiniteMetricEnergy.familyNorm (↑↑(F i) t)

The actual Bochner forcing sum is the literal finite weighted family norm almost everywhere.

theorem EulerWeightedForcingTime.weightedForcingTime_tendsto {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (hT : 0 ≤ T) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : ℕ → A → ↥(EulerTimeLp.TimeLp T (I → H))) (f : A → ↥(EulerTimeLp.TimeLp T (I → H))) (hF : ∀ (i : A), Filter.Tendsto (fun (n : ℕ) => F n i) Filter.atTop (nhds (f i))) : Filter.Tendsto (fun (n : ℕ) => weightedForcingTime T hT w (F n)) Filter.atTop (nhds (weightedForcingTime T hT w f))

Actual finite weighted forcing sums converge strongly with the actual L² forcing fields.

noncomputable def EulerWeightedForcingTime.weightedForcingPath {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → C(↑(Set.Icc 0 T), I → H)) : C(↑(Set.Icc 0 T), ℝ)

The literal weighted forcing norm along continuous time paths.

Equations

• EulerWeightedForcingTime.weightedForcingPath T w F = ∑ i : A, w i * { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerFiniteMetricEnergy.familyNorm ((F i) t), continuous_toFun := ⋯ }

theorem EulerWeightedForcingTime.weightedForcingPath_apply {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → C(↑(Set.Icc 0 T), I → H)) (t : ↑(Set.Icc 0 T)) : (weightedForcingPath T w F) t = ∑ i : A, (w i) t * EulerFiniteMetricEnergy.familyNorm ((F i) t)

The bundled weighted forcing path evaluates to its literal finite norm sum.

theorem EulerWeightedForcingTime.weightedForcingTime_pathLp {A : Type u_1} {I : Type u_2} {H : Type u_3} [Fintype A] [Fintype I] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ℝ) (hT : 0 ≤ T) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → C(↑(Set.Icc 0 T), I → H)) : (weightedForcingTime T hT w fun (i : A) => EulerTimeLp.pathLp T hT (F i)) = EulerTimeLp.pathLp T hT (weightedForcingPath T w F)

Continuous forcing paths have exactly the same weighted norm in the genuine Bochner construction.