Amplitude-generic adapter for the correction tensor recursion.

The hypotheses are primitive seed, temperature, and velocity profiles. The conclusion is the actual I.Amnr field with separate spatial and material rates, so the amplitude can be set from the relative energy scale.

noncomputable def AVenhance.Infra.Section5.RelativeError.relativeAmnrRecursionConstant (β F G Cb : ℝ) : ℝ

The uniform finite-recursion factor in the AMNR tensor estimate.

Equations

• AVenhance.Infra.Section5.RelativeError.relativeAmnrRecursionConstant β F G Cb = 2 ^ (AVenhance.Nstar β + 1) * F * G * (1 + 2 ^ (AVenhance.Nstar β + 1) * Cb) ^ AVenhance.Jcut β

noncomputable def AVenhance.Infra.Section5.RelativeError.relativeMixedTemperatureConstant (β Ccoeff Cb Cd : ℝ) : ℝ

The finite mixed-material induction factor.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.relative_Amnr_mixed_bounds_of_primitive_profiles {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n : ℕ) (j k : Fin 2) {μ : MeasureTheory.Measure Section4.AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))) {L Q F G Cb : ℝ} (hL : 0 ≤ L) (hQ : 0 ≤ Q) (hF : 0 ≤ F) (hG : 0 ≤ G) (hCb : 0 ≤ Cb) (hSeed : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ z ∈ Set.Ioi 0 ×ˢ Set.univ, |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrSeedMultiplier I hΦ m κm n j k i p) z| ≤ F * Section4.amnrWeight L Q w) (hTemperature : ∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)) (r : ℕ), α.length + 2 * r ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α r) (Section4.amnrTGradient (T i) p)) 2 μ ≤ ENNReal.ofReal (G * Section4.amnrWeight L Q (Section4.amnrMixedWord α r))) (hVelocity : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w + 2 ≤ Nstar β → ∀ z ∈ Set.Ioi 0 ×ˢ Set.univ, |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) i p) z| ≤ Cb * Q * Section4.amnrWeight L Q w) (ρ : ℕ) (hρ : ρ ≤ Jcut β) (α : List (Fin 2)) (ℓ : ℕ) (hbudget : α.length + 2 * ℓ ≤ Nstar β - 2 * ρ) (a : Fin 2) : MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α ℓ) fun (y : Section4.AmnrSpace) => I.Amnr hΦ m κm n (T (Nstar β)) ρ y.1 y.2 a j k) 2 μ ≤ ENNReal.ofReal (relativeAmnrRecursionConstant β F G Cb * L ^ α.length * Q ^ (ℓ + ρ))

Primitive amplitude profiles imply the exact mixed-word estimate for the actual AMNR correction tensors. In applications use L = r⁻¹, Q = (tauP)⁻¹, F ≍ ε_m²/κ_m, and G ≍ S/√ν.

theorem AVenhance.Infra.Section5.RelativeError.relative_Amnr_mixed_bounds_of_spatial_profiles {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) (hκprev : 0 < κprev) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n : ℕ) (j k : Fin 2) {μ : MeasureTheory.Measure Section4.AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))) {L Q G Ccoeff Cb Cd F : ℝ} (hL : 0 < L) (hQ : 0 < Q) (hG : 0 ≤ G) (hCcoeff : 0 ≤ Ccoeff) (hCb : 0 ≤ Cb) (hCd : 0 ≤ Cd) (hF : 0 ≤ F) (hRate : κprev * L ^ 2 ≤ Cd * Q) (hCoefficient : ∀ (a p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrTemperatureCoefficient I hΦ m κm κprev a p) z| ≤ Ccoeff * κprev * Section4.amnrWeight L Q w) (hVelocityGradient : ∀ (a p : Fin 2) (α : List (Fin 2)) (r : ℕ), α.length + 2 * r + 2 ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α r) (Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) a p) z| ≤ Cb * Q * Section4.amnrWeight L Q (Section4.amnrMixedWord α r)) (hSpatialGradient : ∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 μ ≤ ENNReal.ofReal (G * L ^ α.length)) (hSeed : ∀ (a p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ z ∈ Set.Ioi 0 ×ˢ Set.univ, |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrSeedMultiplier I hΦ m κm n j k a p) z| ≤ F * Section4.amnrWeight L Q w) (ρ : ℕ) (hρ : ρ ≤ Jcut β) (α : List (Fin 2)) (ℓ : ℕ) (hbudget : α.length + 2 * ℓ ≤ Nstar β - 2 * ρ) (a : Fin 2) : MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α ℓ) fun (y : Section4.AmnrSpace) => I.Amnr hΦ m κm n (T (Nstar β)) ρ y.1 y.2 a j k) 2 μ ≤ ENNReal.ofReal (relativeAmnrRecursionConstant β F (G * relativeMixedTemperatureConstant β Ccoeff Cb Cd ^ Nstar β) Cb * L ^ α.length * Q ^ (ℓ + ρ))

Compose the temperature material induction with the actual correction recursion. The only temperature estimate supplied is the positive-order spatial profile at material level zero; higher material temperature bounds are produced by relative_mixed_material_jets_of_source_profiles.