The actual packet initial increments converge in every finite Sobolev norm to a single smooth field with the same compact support.

Source (22) for a sequence of the actual solved packet increments. Only the source parameter cap and literal scale identities are supplied; all field estimates and the geometric amplitude decay are derived.

theorem EulerPacketInitial.actual_high_summable {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (s : ℕ) : Summable fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum s ((A n).high (EulerPacketSourceScaleSequence.frequency J X n))

theorem EulerPacketInitial.actual_mean_summable {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (s : ℕ) : Summable fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum s ((A n).mean (EulerPacketSourceScaleSequence.frequency J X n))

noncomputable def EulerPacketInitial.Input.increment {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (A : Input U) (k : ℝ) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Increment, given by addField (A.highField k) (A.meanField k).

Equations

• A.increment k = (A.highField k).addField (A.meanField k)

theorem EulerPacketInitial.Input.increment_field {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (A : Input U) (k : ℝ) : (A.increment k).field = A.high k + A.mean k

theorem EulerPacketInitial.Input.increment_norm_le {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (A : Input U) (k : ℝ) (s : ℕ) : EulerOrdinarySobolev.tensorNorm s (A.increment k) ≤ EulerPhysicalL2Scaling.derivativeSum s (A.high k) + EulerPhysicalL2Scaling.derivativeSum s (A.mean k)

theorem EulerPacketInitial.Input.increment_support {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (A : Input U) (k : ℝ) : tsupport (A.increment k).field ⊆ Metric.closedBall 0 2

theorem EulerPacketInitial.actual_increment_summable {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (s : ℕ) : Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm s ((A n).increment (EulerPacketSourceScaleSequence.frequency J X n))

noncomputable def EulerPacketInitial.initialPartial {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (X : ℝ) (N : ℕ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Initial partial, defined pointwise by ∑ n ∈ range N, ((A n).high (frequency J X n) x+(A n).mean (frequency J X n) x).

Equations

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

theorem EulerPacketInitial.initialPartial_field {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (X : ℝ) (N : ℕ) : (EulerSmoothL2Series.partialSum (fun (n : ℕ) => (A n).increment (EulerPacketSourceScaleSequence.frequency J X n)) N).field = initialPartial A J X N

noncomputable def EulerPacketInitial.initialLimit {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Initial limit, constructed using sumField.

Equations

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

theorem EulerPacketInitial.initialLimit_Hm {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (s : ℕ) : Filter.Tendsto (fun (N : ℕ) => EulerPhysicalL2Scaling.derivativeSum s (initialPartial A J X N - (initialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency).field)) Filter.atTop (nhds 0)

theorem EulerPacketInitial.initialLimit_support {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) : tsupport (initialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency).field ⊆ Metric.closedBall 0 2

theorem EulerPacketInitial.initialLimit_compact {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) : HasCompactSupport (initialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency).field

noncomputable def EulerPacketInitial.fullInitialLimit {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (base : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Full initial limit, given by addField base V.

Equations

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

theorem EulerPacketInitial.fullInitialLimit_Hm {U : ℕ → Type} [(n : ℕ) → NormedAddCommGroup (U n)] [(n : ℕ) → InnerProductSpace ℝ (U n)] [∀ (n : ℕ), CompleteSpace (U n)] (A : (n : ℕ) → Input (U n)) (J : ℕ) (hJ : 2 ≤ J) (C c : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (p q : ℕ) (X : ℝ) (hX : 1 ≤ X) (hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n) (hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n) (hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) (hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n) (hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n)) (base : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (s : ℕ) : Filter.Tendsto (fun (N : ℕ) => EulerPhysicalL2Scaling.derivativeSum s (base.field + initialPartial A J X N - (fullInitialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency base).field)) Filter.atTop (nhds 0)