The S-normalised temperature error #
The positive increments telescope to T (Nstar β) - θprev. The abstract
amplitude V estimate is applied with an amplitude tending down to the exact
quantity S = √κprev ‖∇θprev‖; the small positive slack handles S = 0 without
adding a nonvanishing-temperature hypothesis.
@[reducible, inline]
Euclidean-normed real vectors used in the temperature error L² estimates.
Equations
Instances For
def
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperatureEuclideanVec2Lift
(v : Homogenization.Vec 2)
:
View a spatial vector in the Euclidean-normed carrier for the temperature estimates.
Equations
Instances For
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperatureLp_norm_sq_eq_integral
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ : MeasureTheory.Measure α}
{f : α → E}
(hf : MeasureTheory.MemLp f 2 μ)
:
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperatureLp_norm_eq_sqrt_integral
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ : MeasureTheory.Measure α}
{f : α → E}
(hf : MeasureTheory.MemLp f 2 μ)
:
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperature_spaceTimeVectorNormSq_add_le
{F G : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(hF :
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => temperatureEuclideanVec2Lift (F p)) 2
(MeasureTheory.volume.restrict timeCube))
(hG :
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => temperatureEuclideanVec2Lift (G p)) 2
(MeasureTheory.volume.restrict timeCube))
:
√(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (F p + G p)) ≤ √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (F p)) + √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (G p))
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperature_spaceTimeVectorNormSq_finset_sum_le
{ι : Type u_1}
(s : Finset ι)
(F : ι → ℝ × Homogenization.Vec 2 → Homogenization.Vec 2)
(hF :
∀ i ∈ s,
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => temperatureEuclideanVec2Lift (F i p)) 2
(MeasureTheory.volume.restrict timeCube))
:
√(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (∑ i ∈ s, F i p)) ≤ ∑ i ∈ s, √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecNormSq (F i p))
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperature_spaceGrad_finset_sum
{ι : Type u_1}
(s : Finset ι)
(u : ι → ℝ → Homogenization.Vec 2 → ℝ)
(hD : ∀ i ∈ s, ∀ (t : ℝ), 0 < t → Differentiable ℝ (u i t))
(t : ℝ)
(ht : 0 < t)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperature_sqrt_spaceTimeGradNormSq_finset_sum_le
{ι : Type u_1}
(s : Finset ι)
(u : ι → ℝ → Homogenization.Vec 2 → ℝ)
(hD : ∀ i ∈ s, ∀ (t : ℝ), 0 < t → Differentiable ℝ (u i t))
(hLp :
∀ i ∈ s,
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => temperatureEuclideanVec2Lift (spaceGrad (u i p.1) p.2)) 2
(MeasureTheory.volume.restrict timeCube))
:
√(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (fun (y : Homogenization.Vec 2) => ∑ i ∈ s, u i t y) x) ≤ ∑ i ∈ s, √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u i t) x)
def
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperatureErrorClosedCell :
Set (ℝ × Homogenization.Vec 2)
Closed time-space unit cell for the temperature error estimates.
Equations
Instances For
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.temperatureError_memLp_of_continuousOn_closedCell
{E : Type u_1}
[NormedAddCommGroup E]
{f : ℝ × Homogenization.Vec 2 → E}
(hf : ContinuousOn f temperatureErrorClosedCell)
:
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.iterateCoordinateEnergyProfile_mono_amplitude
{u : ℝ → Homogenization.Vec 2 → ℝ}
{κ N N' L : ℝ}
{i : ℕ}
(hκ : 0 < κ)
(hN : 0 ≤ N)
(hNN' : N ≤ N')
(hp : Section4.iterateCoordinateEnergyProfile u κ N L i)
:
Section4.iterateCoordinateEnergyProfile u κ N' L i
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.iterateIncrement_contDiffOn
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
{i : ℕ}
(hi : 1 ≤ i)
(hiN : i ≤ Nstar β)
:
ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => Section4.iterateIncrement T i p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.RelativeError.TemperatureError.iterateIncrement_gradient_memLp
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
{i : ℕ}
(hi : 1 ≤ i)
(hiN : i ≤ Nstar β)
:
MeasureTheory.MemLp
(fun (p : ℝ × Homogenization.Vec 2) =>
temperatureEuclideanVec2Lift (spaceGrad (Section4.iterateIncrement T i p.1) p.2))
2 (MeasureTheory.volume.restrict timeCube)
theorem
AVenhance.Infra.Section5.RelativeError.temperature_error_of_V_zero_bounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
{N η : ℝ}
(hN : 0 ≤ N)
(hη : 0 ≤ η)
(hη1 : η ≤ 1)
(hV :
∀ (i : ℕ),
1 ≤ i →
i ≤ Nstar β →
√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (Section4.iterateIncrement T i s) x) ≤ N * Section4.iterateAmplitude η i * ↑(2 * i).factorial)
:
Finite positive-increment telescope in the spacetime gradient norm.
The only quantitative input is the zeroth-word slice of l.V; the base
profile is absent because the difference is the sum over i ≥ 1.
theorem
AVenhance.Infra.Section5.RelativeError.temperatureError_leaf_of_abstract_V
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 2 ≤ m)
(hκm : 0 < κm)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : Section4.AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
(hA3 :
∀ (j : ℕ),
1 ≤ j →
∀ (t : ℝ) (n : ℕ),
2 ≤ n →
barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3)))
{c Ck K Cflow Cmean Rflow Cθ Rθ C₀ Ct : ℝ}
(hc : 0 < c)
(hCk : 0 ≤ Ck)
(hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hCm : 0 ≤ Cmean)
(hRf : 256 ≤ Rflow)
(hRθ : 0 < Rθ)
(hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κprev)
(hupper : κprev ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(hC₀ :
Section4.iterateSourceConstant (Section4.iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀)
(hsmall :
C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2)) ≤ 1)
(hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev)
(hmean :
∀ (j k : Fin 2), |(timeAvgMat (I.Kmat κm m) - κprev • 1) j k| ≤ κprev * Cmean * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hzero :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hpositive :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (p : List (Fin 2)),
1 ≤ p.length →
∀ (j k : Fin 2),
|Section4.iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length)
(hκscale : |κm| ≤ κprev)
(hLater : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ Rθ)
(hbase :
Section4.iterateCoordinateEnergyProfile θprev κprev
(√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
(max (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (C₀ / Rθ)) 0)
(hCt : ↑(Nstar β) * ↑(2 * Nstar β).factorial * C₀ ^ 3 ≤ Ct)
:
The hTemperatureError leaf with the exact S-normalisation of .
hbase is the scale-S theta profile in the precise shape
consumed by abstract l.V. The flow, coefficient and smallness hypotheses are
likewise kept in the exact shapes consumed there. hCt allows the surrounding
RelativeLeaves record to choose any constant at least the explicit bound.