Literal metric, loss, and forcing paths for the actual full-order word regularization.

noncomputable def EulerRegularizedMetricPaths.metricOperatorPath (period : ℝ) [Fact (0 < period)] (T : ℝ) (K : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period) (hK : Continuous fun (t : ↑(Set.Icc 0 T)) => (K t).operator) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

A genuine continuous path of L² multipliers from the given actual smooth coefficient family.

Equations

• EulerRegularizedMetricPaths.metricOperatorPath period T K hK = { toFun := fun (t : ↑(Set.Icc 0 T)) => (K t).operator, continuous_toFun := hK }

theorem EulerRegularizedMetricPaths.coefficient_path_integrable (T : ℝ) (hT : 0 ≤ T) (w a b : C(↑(Set.Icc 0 T), ℝ)) (n : ℕ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerVolterraConvolution.extendPath T hT w r * EulerVolterraConvolution.extendPath T hT a r + EulerVolterraConvolution.extendPath T hT b r * ↑n * EulerVolterraConvolution.extendPath T hT w r) (Set.Icc 0 T) MeasureTheory.volume

The literal scalar metric-growth and radius-loss coefficients are integrable for continuous time paths.

theorem EulerRegularizedMetricPaths.forcing_path_integrable (period : ℝ) [Fact (0 < period)] {β : Type u_1} [Fintype β] (T : ℝ) (hT : 0 ≤ T) (w d : C(↑(Set.Icc 0 T), ℝ)) (f : C(↑(Set.Icc 0 T), β → ↥(EulerLiftedGradientSpace.LiftL2 period))) : MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerVolterraConvolution.extendPath T hT w r * (EulerVolterraConvolution.extendPath T hT d r * EulerFiniteMetricEnergy.familyNorm (EulerVolterraConvolution.extendPath T hT f r))) (Set.Icc 0 T) MeasureTheory.volume

The literal finite forcing coefficient is integrable for genuine continuous family paths.

theorem EulerRegularizedMetricPaths.regularized_metric_path_eq (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (order : α → ℕ) (R : C(↑(Set.Icc 0 T), ℝ)) (K : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period) (hK : Continuous fun (t : ↑(Set.Icc 0 T)) => (K t).operator) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (r : ℝ) : (EulerWeightedCylinderEnergy.weightedMetricSum (EulerVolterraConvolution.extendPath T hT R r) order (K (Set.projIcc 0 T hT r)).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT (EulerRegularizedWordEquation.regularizedWordPath period ⋯ n (w i j) T u) r)) = EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T (fun (i : α) => EulerSobolevEnergyPaths.gevreyWeightPath T R (order i)) (metricOperatorPath period T K hK) (EulerRegularizedEnergyFamily.regularizedValueFamily period d w hd n T u)) r

The computed metric path is exactly the actual factorial-weighted metric sum on the regularized fields.

theorem EulerRegularizedMetricPaths.regularized_loss_path_eq (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (order : α → ℕ) (R : C(↑(Set.Icc 0 T), ℝ)) (K : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period) (hK : Continuous fun (t : ↑(Set.Icc 0 T)) => (K t).operator) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (r : ℝ) : (EulerWeightedCylinderEnergy.weightedMetricLoss (EulerVolterraConvolution.extendPath T hT R r) order (K (Set.projIcc 0 T hT r)).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT (EulerRegularizedWordEquation.regularizedWordPath period ⋯ n (w i j) T u) r)) = EulerVolterraConvolution.extendPath T hT (EulerMetricPathConvergence.weightedMetricPath T (fun (i : α) => EulerSobolevEnergyPaths.gevreyLossWeightPath T R (order i)) (metricOperatorPath period T K hK) (EulerRegularizedEnergyFamily.regularizedValueFamily period d w hd n T u)) r

The computed radius-loss path is exactly the actual order-weighted metric sum.

theorem EulerRegularizedMetricPaths.regularized_forcing_path_eq (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (order : α → ℕ) (R : C(↑(Set.Icc 0 T), ℝ)) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (r : ℝ) : (EulerWeightedCylinderEnergy.weightedForcingSum (EulerVolterraConvolution.extendPath T hT R r) order fun (i : α) (j : β) => EulerVolterraConvolution.extendPath T hT (EulerRegularizedForcingWord.forcingWordPath period ⋯ n (w i j) T A G u f p) r) = EulerVolterraConvolution.extendPath T hT (EulerWeightedForcingTime.weightedForcingPath T (fun (i : α) => EulerSobolevEnergyPaths.gevreyWeightPath T R (order i)) (EulerRegularizedEnergyFamily.regularizedForcingFamily period d w hd n T A G u f p)) r

The computed forcing path is exactly the actual weighted family norm of the regularized PDE forcing.