Genuine continuous energy paths and their weighted strong limits.

noncomputable def EulerSobolevEnergyPaths.familyValueOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) {I : Type u_1} : (I → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) →L[ℝ] I → ↥(EulerLiftedGradientSpace.LiftL2 period)

Underlying L² values of a finite actual Sobolev family form a bounded linear map.

Equations

• EulerSobolevEnergyPaths.familyValueOperator period q = ContinuousLinearMap.pi fun (i : I) => EulerCylinderSobolevSpace.valueOperator period q ∘SL ContinuousLinearMap.proj i

noncomputable def EulerSobolevEnergyPaths.familyValuePath (period : ℝ) [Fact (0 < period)] (q : ℕ) {I : Type u_1} (T : ℝ) (u : C(↑(Set.Icc 0 T), I → ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), I → ↥(EulerLiftedGradientSpace.LiftL2 period))

The genuine L² field-family path underlying an actual Sobolev family path.

Equations

• EulerSobolevEnergyPaths.familyValuePath period q T u = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerSobolevEnergyPaths.familyValueOperator period q)) u

theorem EulerSobolevEnergyPaths.familyValuePath_apply (period : ℝ) [Fact (0 < period)] (q : ℕ) {I : Type u_1} (T : ℝ) (u : C(↑(Set.Icc 0 T), I → ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) (i : I) : (familyValuePath period q T u) t i = EulerCylinderSobolevSpace.value period (u t i)

Family-path values are the literal underlying L² values of the Sobolev fields.

noncomputable def EulerSobolevEnergyPaths.gevreyWeightPath (T : ℝ) (ρ : C(↑(Set.Icc 0 T), ℝ)) (n : ℕ) : C(↑(Set.Icc 0 T), ℝ)

The actual factorial Gevrey weight along a continuous radius path.

Equations

• EulerSobolevEnergyPaths.gevreyWeightPath T ρ n = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerPacketWeights.weight (ρ t) n, continuous_toFun := ⋯ }

noncomputable def EulerSobolevEnergyPaths.gevreyLossWeightPath (T : ℝ) (ρ : C(↑(Set.Icc 0 T), ℝ)) (n : ℕ) : C(↑(Set.Icc 0 T), ℝ)

The actual radius-loss weight along the same radius path.

Equations

• EulerSobolevEnergyPaths.gevreyLossWeightPath T ρ n = ↑n • EulerSobolevEnergyPaths.gevreyWeightPath T ρ n

theorem EulerSobolevEnergyPaths.forcing_integral_eq (period : ℝ) [Fact (0 < period)] {A : Type u_1} {I : Type u_2} [Fintype A] [Fintype I] (T : ℝ) (hT : 0 ≤ T) (c : C(↑(Set.Icc 0 T), ℝ)) (w : A → C(↑(Set.Icc 0 T), ℝ)) (F : A → C(↑(Set.Icc 0 T), I → ↥(EulerLiftedGradientSpace.LiftL2 period))) : ∫ (t : ℝ), ↑↑(EulerTimeLp.pathLp T hT c) t * ↑↑(EulerWeightedForcingTime.weightedForcingTime T hT w fun (i : A) => EulerTimeLp.pathLp T hT (F i)) t ∂EulerTimeLp.timeMeasure T = ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT c t * EulerVolterraConvolution.extendPath T hT (EulerWeightedForcingTime.weightedForcingPath T w F) t

A continuous-path weighted forcing integral is exactly its genuine Bochner forcing pairing.

theorem EulerSobolevEnergyPaths.weighted_energy_limit (period : ℝ) [Fact (0 < period)] {A : Type u_1} {I : Type u_2} [Fintype A] [Fintype I] (T : ℝ) (hT : 0 ≤ T) (w loss : A → C(↑(Set.Icc 0 T), ℝ)) (K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (a b c : C(↑(Set.Icc 0 T), ℝ)) (E F : ℕ → A → C(↑(Set.Icc 0 T), I → ↥(EulerLiftedGradientSpace.LiftL2 period))) (e : A → C(↑(Set.Icc 0 T), I → ↥(EulerLiftedGradientSpace.LiftL2 period))) (f : A → ↥(EulerTimeLp.TimeLp T (I → ↥(EulerLiftedGradientSpace.LiftL2 period)))) (hE : ∀ (i : A), Filter.Tendsto (fun (n : ℕ) => E n i) Filter.atTop (nhds (e i))) (hF : ∀ (i : A), Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (F n i)) Filter.atTop (nhds (f i))) (henergy : ∀ (n : ℕ), (EulerMetricPathConvergence.weightedMetricPath T w K (E n)) ⟨T, ⋯⟩ - (EulerMetricPathConvergence.weightedMetricPath T w K (E n)) ⟨0, ⋯⟩ ≤ ((∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T w K (E n)) t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T loss K (E n)) t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT c t * EulerVolterraConvolution.extendPath T hT (EulerWeightedForcingTime.weightedForcingPath T w (F n)) t) : (EulerMetricPathConvergence.weightedMetricPath T w K e) ⟨T, ⋯⟩ - (EulerMetricPathConvergence.weightedMetricPath T w K e) ⟨0, ⋯⟩ ≤ ((∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T w K e) t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T loss K e) t) + ∫ (t : ℝ), ↑↑(EulerTimeLp.pathLp T hT c) t * ↑↑(EulerWeightedForcingTime.weightedForcingTime T hT w f) t ∂EulerTimeLp.timeMeasure T

Finite actual weighted metric energy passes through uniform field limits and strong L² forcing limits, preserving the signed radius-loss integral.