Linearized complex physical tensor path

Fixing a complex physical L² path in the first factor gives a continuous complex tensor path, linear in the second factor.

noncomputable def CKN.Leray.regularisedComplexLinearTensorPath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (g v : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) : ℝ → ↥ComplexTensorL2

The clamped physical tensor path with a prescribed physical L² first factor and an unknown complex physical second factor.

Equations

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

theorem CKN.Leray.regularisedComplexLinearTensorPath_continuous (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (g v : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) : Continuous (regularisedComplexLinearTensorPath ρ ε hε T hT g v)

The prescribed L² path and complex physical path produce a continuous physical tensor path.

theorem CKN.Leray.regularisedComplexLinearTensorPath_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (g v : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (B : ℝ) (hB : 0 ≤ B) (hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B) (s : ℝ) : ‖regularisedComplexLinearTensorPath ρ ε hε T hT g v s‖ ≤ regularisedTensorPhysicalConstant ρ ε hε * B * ‖v‖

A uniform physical L² bound makes the linearized tensor path bounded linearly in the complex physical trajectory norm.

theorem CKN.Leray.regularisedComplexLinearTensorPath_sub (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (g u v : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (s : ℝ) : regularisedComplexLinearTensorPath ρ ε hε T hT g (u - v) s = regularisedComplexLinearTensorPath ρ ε hε T hT g u s - regularisedComplexLinearTensorPath ρ ε hε T hT g v s

The physical tensor path is linear in its second trajectory.