Positive-time existence for the actual projected quadratic cylinder correction equation.

def EulerQuadraticSource.timeInclusion {T S : ℝ} (hTS : T ≤ S) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 S))

Inclusion of a shorter initial time interval into a prescribed positive interval.

Equations

• EulerQuadraticSource.timeInclusion hTS = { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨↑t, ⋯⟩, continuous_toFun := ⋯ }

@[instance_reducible]

noncomputable def EulerQuadraticSource.sobolevGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerQuadraticSource.sobolevGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerQuadraticSource.sobolevRealSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerQuadraticSource.sobolevRealSpace period q = inferInstance

noncomputable def EulerQuadraticSource.quadraticDuhamel (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) {S T : ℝ} (hT : 0 ≤ T) (hTS : T ≤ S) (C : Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))

The genuine heat Duhamel expression for continuous projected quadratic coefficients.

Equations

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

theorem EulerQuadraticSource.exists_local_quadratic_mild (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (C : Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ∃ (T : ℝ) (hT : 0 < T) (hTS : T ≤ S) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖u‖ ≤ ‖u₀‖ + 1 ∧ u ⟨0, ⋯⟩ = u₀ ∧ ∀ (t : ↑(Set.Icc 0 T)), u t = quadraticDuhamel period ν hν ⋯ hTS C u₀ u t

Continuous actual linear and quadratic coefficients yield a mild solution on a strictly positive time interval.