Constructed spatial L² evolution from the coefficient field alone

The bounded-field Banach algebra supplies actual fundamental fields by the proved Picard construction. Their multiplication operators give an actual evolution on supported spatial L². The localized H3 estimate is imposed only on this genuine homogeneous propagator and is then inherited with constant one by the spatial L² evolution.

Lifting the localized homogeneous propagator to actual spatial L²

The homogeneous fundamental fields are multiplied against genuine spatial L² functions supported in a fixed measurable set. The resulting continuous operator paths satisfy the homogeneous differential equation and inverse identities. Their propagator norm uses only the pointwise bound on that set, so the source's C g(t)/g(s) estimate is preserved exactly.

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution1 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing (V →L[ℝ] V)

Cache the standard NormedRing (V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution2 {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing EulerLpSupportedMultiplier.Field

Cache the standard NormedRing (Field (α := α) (V := V)) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution3 {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAddCommGroup EulerLpSupportedMultiplier.Field

Cache the standard NormedAddCommGroup (Field (α := α) (V := V)) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution4 {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ EulerLpSupportedMultiplier.Field

Cache the standard NormedSpace ℝ (Field (α := α) (V := V)) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution5 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] : NormedAddCommGroup ↥(MeasureTheory.Lp V 2 μ)

Cache the standard NormedAddCommGroup (Lp V 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution5 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution6 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] : InnerProductSpace ℝ ↥(MeasureTheory.Lp V 2 μ)

Cache the standard InnerProductSpace ℝ (Lp V 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution6 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution7 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard NormedAddCommGroup (supportedSpace (V := V) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution7 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution8 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : InnerProductSpace ℝ ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard InnerProductSpace ℝ (supportedSpace (V := V) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution8 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution9 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard NormedSpace ℝ (supportedSpace (V := V) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution9 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution10 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedAddCommGroup (↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS))

Cache the standard NormedAddCommGroup (supportedSpace (V := V) μ S hS →L[ℝ] supportedSpace (V := V) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution10 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedEvolution.instLpSupportedEvolution11 {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : NormedSpace ℝ (↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS))

Cache the standard NormedSpace ℝ (supportedSpace (V := V) μ S hS →L[ℝ] supportedSpace (V := V) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedEvolution.instLpSupportedEvolution11 μ S hS = inferInstance

noncomputable def EulerLpSupportedEvolution.operatorPath {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) : C(↑(Set.Icc 0 T), ↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS))

The actual supported-space operator associated with a continuous field path.

Equations

• EulerLpSupportedEvolution.operatorPath μ S hS T A = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerLpSupportedMultiplier.operator μ S hS (A t), continuous_toFun := ⋯ }

@[simp]

theorem EulerLpSupportedEvolution.operatorPath_apply {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (t : ↑(Set.Icc 0 T)) : (operatorPath μ S hS T A) t = EulerLpSupportedMultiplier.operator μ S hS (A t)

theorem EulerLpSupportedEvolution.operatorPath_hasDerivWithinAt {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (operatorPath μ S hS T A)) ((operatorPath μ S hS T A') t) (Set.Icc 0 T) ↑t

Actual pointwise time derivatives lift to supported-L² operator derivatives.

noncomputable def EulerLpSupportedEvolution.liftEvolution {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B Φ Ψ : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (hRight : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Φ t) x ∘SL (Ψ t) x = ContinuousLinearMap.id ℝ V) (hLeft : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Ψ t) x ∘SL (Φ t) x = ContinuousLinearMap.id ℝ V) (hΦ : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Φ s) x) ((EulerVolterraConvolution.extendPath T hT B t) x ∘SL (EulerVolterraConvolution.extendPath T hT Φ t) x) (Set.Icc 0 T) t) : EulerLinearDuhamel.Evolution T hT (operatorPath μ S hS T B)

The actual pointwise homogeneous fields give a homogeneous evolution on the genuine supported spatial L² space.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerLpSupportedEvolution.liftEvolution_propagator_norm {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B Φ Ψ : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (hRight : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Φ t) x ∘SL (Ψ t) x = ContinuousLinearMap.id ℝ V) (hLeft : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Ψ t) x ∘SL (Φ t) x = ContinuousLinearMap.id ℝ V) (hΦ : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Φ s) x) ((EulerVolterraConvolution.extendPath T hT B t) x ∘SL (EulerVolterraConvolution.extendPath T hT Φ t) x) (Set.Icc 0 T) t) (g : ↑(Set.Icc 0 T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (C : ℝ) (hC : 0 ≤ C) (hprop : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ x ∈ S, ‖(Φ t) x ∘SL (Ψ s) x‖ ≤ C * g t / g s) (t s : ↑(Set.Icc 0 T)) (hst : s ≤ t) : ‖(liftEvolution μ S hS T hT B Φ Ψ hRight hLeft hΦ).propagator t s‖ ≤ C * g t / g s

The pointwise localized (H3) estimate is the actual L² propagator norm, with the identical relative profile factor.

theorem EulerLpSupportedEvolution.liftedSolution_profile_bound {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B Φ Ψ : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (hRight : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Φ t) x ∘SL (Ψ t) x = ContinuousLinearMap.id ℝ V) (hLeft : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Ψ t) x ∘SL (Φ t) x = ContinuousLinearMap.id ℝ V) (hΦ : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Φ s) x) ((EulerVolterraConvolution.extendPath T hT B t) x ∘SL (EulerVolterraConvolution.extendPath T hT Φ t) x) (Set.Icc 0 T) t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpSupportedSubspace.supportedSpace μ S hS))) (a₀ : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) (g : ↑(Set.Icc 0 T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hg₀ : g ⟨0, ⋯⟩ = 1) (C D : ℝ) (hC : 0 ≤ C) (hprop : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ x ∈ S, ‖(Φ t) x ∘SL (Ψ s) x‖ ≤ C * g t / g s) (hf : ∀ (s : ↑(Set.Icc 0 T)), ‖f s‖ ≤ D * g s) (t : ↑(Set.Icc 0 T)) : ‖((liftEvolution μ S hS T hT B Φ Ψ hRight hLeft hΦ).solution f a₀) t‖ ≤ C * g t * (‖a₀‖ + ↑t * D)

The actual forced supported-L² path has the source's polynomial profile bound.

theorem EulerLpSupportedEvolution.liftedSolution_hasDerivWithinAt {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set α) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B Φ Ψ : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (hRight : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Φ t) x ∘SL (Ψ t) x = ContinuousLinearMap.id ℝ V) (hLeft : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∈ S, (Ψ t) x ∘SL (Φ t) x = ContinuousLinearMap.id ℝ V) (hΦ : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Φ s) x) ((EulerVolterraConvolution.extendPath T hT B t) x ∘SL (EulerVolterraConvolution.extendPath T hT Φ t) x) (Set.Icc 0 T) t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpSupportedSubspace.supportedSpace μ S hS))) (a₀ : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((liftEvolution μ S hS T hT B Φ Ψ hRight hLeft hΦ).solution f a₀)) ((EulerLpSupportedMultiplier.operator μ S hS (B t)) (((liftEvolution μ S hS T hT B Φ Ψ hRight hLeft hΦ).solution f a₀) t) + f t) (Set.Icc 0 T) ↑t

This profile-bounded path solves the actual supported-L² differential equation.

@[instance_reducible]

noncomputable def EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution1 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing (V →L[ℝ] V)

Cache the standard NormedRing (V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution2 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAlgebra ℝ (V →L[ℝ] V)

Cache the standard NormedAlgebra ℝ (V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution3 {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing EulerLpSupportedMultiplier.Field

Cache the standard NormedRing (Field (α := α) (V := V)) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution4 {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAlgebra ℝ EulerLpSupportedMultiplier.Field

Cache the standard NormedAlgebra ℝ (Field (α := α) (V := V)) instance to shorten typeclass synthesis.

Equations

• EulerLpSupportedConstructedEvolution.instLpSupportedConstructedEvolution4 = inferInstance

theorem EulerLpSupportedConstructedEvolution.fundamental_pointwise_derivative {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (x : α) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT (EulerLinearFundamentalExistence.fundamentalPath T hT B).forward s) x) ((EulerVolterraConvolution.extendPath T hT B t) x ∘SL (EulerVolterraConvolution.extendPath T hT (EulerLinearFundamentalExistence.fundamentalPath T hT B).forward t) x) (Set.Icc 0 T) t

The constructed fields satisfy the literal pointwise homogeneous ODE.

noncomputable def EulerLpSupportedConstructedEvolution.constructedSupportedEvolution {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) : EulerLinearDuhamel.Evolution T hT (EulerLpSupportedEvolution.operatorPath μ S hS T B)

A genuine supported-L² evolution constructed from the original bounded coefficient.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerLpSupportedConstructedEvolution.constructedSupportedEvolution_propagator_norm {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) (g : ↑(Set.Icc 0 T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (C : ℝ) (hC : 0 ≤ C) (hprop : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ x ∈ S, ‖((EulerLinearFundamentalExistence.fundamentalPath T hT B).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT B).backward s) x‖ ≤ C * g t / g s) (t s : ↑(Set.Icc 0 T)) (hst : s ≤ t) : ‖(constructedSupportedEvolution T hT B μ S hS).propagator t s‖ ≤ C * g t / g s

The actual supported-L² propagator retains the exact localized H3 bound.