Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.BaseEnergyIdentity

integrated energy identity for classical solutions #

For an admissible stream φ, a classical solution θ with zero forcing and mean-zero smooth periodic datum g satisfies, for t ∈ [0,1], ‖θ(t)‖² + 2κ ∫_0^t ‖∇θ(s)‖² ds = ‖g‖², the mean of θ(t) vanishes, and the spaceTimeGradNormSq equals ∫_0^1 ‖∇θ(s)‖² ds.

source
theorem AVenhance.Infra.Section5.RelativeError.integral_cell_shift_sq {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) :
∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (f x + 1) ^ 2 = ((∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x ^ 2) + 2 * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x) + ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, 1

∫_cell (f + 1)² = ∫_cell f² + 2 ∫_cell f + ∫_cell 1 for continuous f.

source
noncomputable def AVenhance.Infra.Section5.RelativeError.cellGrad (θ : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) :
ℝ

The cell integral ∫_cell |∇θ(s)|².

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Section5.RelativeError.shift_energy_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) (c : ℝ) {T : ℝ} (hT : 0 ≤ T) :
    ContinuousOn (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (θ s x + c) ^ 2) (Set.Icc 0 T)

    Energy of a shifted solution is continuous on [0,T].

    source
    theorem AVenhance.Infra.Section5.RelativeError.cellGrad_eq_sum {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {s : ℝ} (hs : 0 ≤ s) :
    cellGrad θ s = (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, spaceGrad (θ s) x 0 ^ 2) + ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, spaceGrad (θ s) x 1 ^ 2

    cellGrad splits as the sum of the squared component integrals.

    source
    theorem AVenhance.Infra.Section5.RelativeError.cellGrad_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {T : ℝ} (hT : 0 ≤ T) :
    ContinuousOn (cellGrad θ) (Set.Icc 0 T)

    cellGrad is continuous on [0,T].

    source
    theorem AVenhance.Infra.Section5.RelativeError.classical_meanZero {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) (hg : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x = 0) {t : ℝ} (ht : 0 ≤ t) :
    ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, θ t x = 0

    The mean of a classical solution with mean-zero datum vanishes at every nonnegative time.