TJets #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section5.Contracts.tJets_of_thetaProfile_contract
(β Ccut CsReq : ℝ)
:
∃ (Cs : ℝ) (A : ℝ) (C₁ : ℝ),
CsReq ≤ Cs ∧ 1 ≤ Cs ∧ 1 ≤ A ∧ Integration.OnA7Instances β Ccut C₁
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ)
(R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
∀ (N : ℝ),
0 ≤ N →
Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs N →
Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A N ∧ Integration.TPositiveJetsContract I m T A N ∧ Integration.FirstOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A N ∧ Integration.FirstOrderSliceJetContract I m T (A ^ 2) N ∧ Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs R N
All abstract-amplitude T and V contracts from the sole remaining theta profile. The profile coefficient may exceed any requested lower bound. Every coefficient and the scale threshold precedes the ingredients.
theorem
AVenhance.Infra.Section5.Contracts.firstOrderSliceJet_contract
(β Ccut : ℝ)
:
∃ (AT : ℝ) (C₁ : ℝ),
Integration.OnA7Instances β Ccut C₁
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (_κ : ℝ) (_M : ℕ) (_R : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
Integration.FirstOrderSliceJetContract I m T AT √(l2NormSq θ₀)
The unconditional N-normalised ansatz jet, in the family block.
theorem
AVenhance.Infra.Section5.Contracts.tGradient_contract
(β Ccut : ℝ)
:
∃ (A : ℝ) (C₁ : ℝ),
Integration.OnA7Instances β Ccut C₁
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ) (_m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
Integration.TGradientContract β (I.kappaSeq κ M (_m - 1)) T A √(l2NormSq θ₀)
The unconditional N-normalised integrated T gradient.