Periodic Cutoff

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Heat.heatPeriodicCutoff (x : ℝ) : ℝ

A smooth, compactly supported partition-of-unity weight for the unit period.

Equations

• AVenhance.Infra.Heat.heatPeriodicCutoff x = (x + 1).smoothTransition - x.smoothTransition

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff_partition {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : heatPeriodicCutoff (x - 1) + heatPeriodicCutoff x = 1

noncomputable def AVenhance.Infra.Heat.heatPeriodicCutoff2 (x : Homogenization.Vec 2) : ℝ

The product cutoff on Vec 2; its four translates cover a unit cell.

Equations

• AVenhance.Infra.Heat.heatPeriodicCutoff2 x = AVenhance.Infra.Heat.heatPeriodicCutoff (x 0) * AVenhance.Infra.Heat.heatPeriodicCutoff (x 1)

def AVenhance.Infra.Heat.heatPeriodicTileShift (b : Bool × Bool) : Fin 2 → ℤ

The four unit-cell shifts needed to cover the support of the product cutoff.

Equations

• AVenhance.Infra.Heat.heatPeriodicTileShift b i = if i = 0 then if b.1 = true then 0 else -1 else if b.2 = true then 0 else -1

def AVenhance.Infra.Heat.heatPeriodicTileStart (b : Bool × Bool) : Fin 2 → ℝ

Integer-vector starting point of one periodic heat tile.

Equations

• AVenhance.Infra.Heat.heatPeriodicTileStart b = AVenhance.Infra.Torus.intVector (AVenhance.Infra.Heat.heatPeriodicTileShift b)

def AVenhance.Infra.Heat.heatPeriodicTile (b : Bool × Bool) : Set (Homogenization.Vec 2)

Translated unit cell associated with a periodic heat tile.

Equations

• AVenhance.Infra.Heat.heatPeriodicTile b = AVenhance.Infra.Torus.unitCellAt 2 (AVenhance.Infra.Heat.heatPeriodicTileStart b)

noncomputable def AVenhance.Infra.Heat.PeriodicCutoff.heatShiftedCutoff (b : Bool) (x : ℝ) : ℝ

Translate the one-dimensional periodic heat cutoff according to the Boolean tile index.

Equations

• AVenhance.Infra.Heat.PeriodicCutoff.heatShiftedCutoff b x = AVenhance.Infra.Heat.heatPeriodicCutoff (x + if b = true then 0 else -1)

theorem AVenhance.Infra.Heat.PeriodicCutoff.sum_heatShiftedCutoff {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ∑ b : Bool, heatShiftedCutoff b x = 1

theorem AVenhance.Infra.Heat.sum_heatPeriodicCutoff2_translates {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, heatPeriodicCutoff2 (x + Torus.intVector (heatPeriodicTileShift b)) = 1

On the unit square, the four translates of the product cutoff sum to one.

theorem AVenhance.Infra.Heat.heatPeriodicCutoff_contDiff : ContDiff ℝ (↑⊤) heatPeriodicCutoff

theorem AVenhance.Infra.Heat.heatPeriodicCutoff2_contDiff : ContDiff ℝ (↑⊤) heatPeriodicCutoff2

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff_nonneg (x : ℝ) : 0 ≤ heatPeriodicCutoff x

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff_at_edges (x : ℝ) (hx : x = -1 ∨ x = 1) : heatPeriodicCutoff x = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff2_nonneg (x : Homogenization.Vec 2) : 0 ≤ heatPeriodicCutoff2 x

theorem AVenhance.Infra.Heat.PeriodicCutoff.fderiv_heatPeriodicCutoff_coord (i j : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => heatPeriodicCutoff (y j)) x) (Homogenization.basisVec i) = if i = j then deriv heatPeriodicCutoff (x j) else 0

theorem AVenhance.Infra.Heat.fderiv_heatPeriodicCutoff2 (i : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ heatPeriodicCutoff2 x) (Homogenization.basisVec i) = if i = 0 then deriv heatPeriodicCutoff (x 0) * heatPeriodicCutoff (x 1) else heatPeriodicCutoff (x 0) * deriv heatPeriodicCutoff (x 1)

theorem AVenhance.Infra.Heat.abs_heatPeriodicCutoff_le_one (x : ℝ) : |heatPeriodicCutoff x| ≤ 1

theorem AVenhance.Infra.Heat.norm_heatPeriodicCutoff2_le_one (x : Homogenization.Vec 2) : ‖heatPeriodicCutoff2 x‖ ≤ 1

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff_support : Function.support heatPeriodicCutoff ⊆ Set.Ioc (-1) 1

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff2_support : Function.support heatPeriodicCutoff2 ⊆ Set.univ.pi fun (x : Fin 2) => Set.Ioc (-1) 1

def AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff2ClosedBox : Set (Homogenization.Vec 2)

Closed box containing the support of the two-dimensional periodic heat cutoff.

Equations

• AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff2ClosedBox = Set.univ.pi fun (x : Fin 2) => Set.Icc (-1) 1

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicCutoff2_tsupport_subset_closedBox : tsupport heatPeriodicCutoff2 ⊆ heatPeriodicCutoff2ClosedBox

theorem AVenhance.Infra.Heat.heatPeriodicCutoff2_hasCompactSupport : HasCompactSupport heatPeriodicCutoff2

theorem AVenhance.Infra.Heat.heatPeriodicCutoff2_coordDeriv_support (i : Fin 2) : (Function.support fun (x : Homogenization.Vec 2) => (fderiv ℝ heatPeriodicCutoff2 x) (Homogenization.basisVec i)) ⊆ Set.univ.pi fun (x : Fin 2) => Set.Ioc (-1) 1

theorem AVenhance.Infra.Heat.PeriodicCutoff.mem_biUnion_heatPeriodicTile_of_mem_box {x : Homogenization.Vec 2} (hx : x ∈ Set.univ.pi fun (x : Fin 2) => Set.Ioc (-1) 1) : x ∈ ⋃ (b : Bool × Bool), heatPeriodicTile b

theorem AVenhance.Infra.Heat.PeriodicCutoff.heatPeriodicTile_disjoint {b c : Bool × Bool} (hbc : b ≠ c) : Disjoint (heatPeriodicTile b) (heatPeriodicTile c)

theorem AVenhance.Infra.Heat.PeriodicCutoff.measurable_heatPeriodicTile (b : Bool × Bool) : MeasurableSet (heatPeriodicTile b)

theorem AVenhance.Infra.Heat.heatPeriodicCutoff2_support_subset_tiles : Function.support heatPeriodicCutoff2 ⊆ ⋃ (b : Bool × Bool), heatPeriodicTile b

theorem AVenhance.Infra.Heat.heatPeriodicCutoff2_coordDeriv_support_subset_tiles (i : Fin 2) : (Function.support fun (x : Homogenization.Vec 2) => (fderiv ℝ heatPeriodicCutoff2 x) (Homogenization.basisVec i)) ⊆ ⋃ (b : Bool × Bool), heatPeriodicTile b

theorem AVenhance.Infra.Heat.heatPeriodicCutoff_deriv_partition {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : deriv heatPeriodicCutoff (x - 1) + deriv heatPeriodicCutoff x = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_smoothTransition_zero_of_value {x : ℝ} (hx : x.smoothTransition = 0) : deriv Real.smoothTransition x = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_smoothTransition_one_of_value {x : ℝ} (hx : x.smoothTransition = 1) : deriv Real.smoothTransition x = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_heatPeriodicCutoff (x : ℝ) : deriv heatPeriodicCutoff x = deriv Real.smoothTransition (x + 1) - deriv Real.smoothTransition x

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_heatPeriodicCutoff_at_left : deriv heatPeriodicCutoff (-1) = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_heatPeriodicCutoff_at_zero : deriv heatPeriodicCutoff 0 = 0

theorem AVenhance.Infra.Heat.PeriodicCutoff.deriv_heatPeriodicCutoff_at_right : deriv heatPeriodicCutoff 1 = 0

theorem AVenhance.Infra.Heat.heatPeriodicCutoff_deriv_partition_closed {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : deriv heatPeriodicCutoff (x - 1) + deriv heatPeriodicCutoff x = 0

noncomputable def AVenhance.Infra.Heat.PeriodicCutoff.heatShiftedCutoffDerivative (b : Bool) (x : ℝ) : ℝ

Translated derivative of the one-dimensional periodic heat cutoff.

Equations

• AVenhance.Infra.Heat.PeriodicCutoff.heatShiftedCutoffDerivative b x = deriv AVenhance.Infra.Heat.heatPeriodicCutoff (x + if b = true then 0 else -1)

theorem AVenhance.Infra.Heat.PeriodicCutoff.sum_heatShiftedCutoffDerivative {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ∑ b : Bool, heatShiftedCutoffDerivative b x = 0

theorem AVenhance.Infra.Heat.sum_heatPeriodicCutoff2_coordDeriv_translates (i : Fin 2) {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, (fderiv ℝ heatPeriodicCutoff2 (x + Torus.intVector (heatPeriodicTileShift b))) (Homogenization.basisVec i) = 0

theorem AVenhance.Infra.Heat.integral_unitCellAt_translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Homogenization.Vec 2 → E) (a : Fin 2 → ℝ) : ∫ (x : Homogenization.Vec 2) in Torus.unitCellAt 2 a, F x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, F (x + a)

Translate a cell integral back to the canonical unit cell.

theorem AVenhance.Infra.Heat.integrable_unitCellAt_translate {E : Type u_1} [NormedAddCommGroup E] {F : Homogenization.Vec 2 → E} {a : Fin 2 → ℝ} (hF : MeasureTheory.IntegrableOn F (Torus.unitCellAt 2 a) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => F (x + a)) (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Heat.memLp_periodic_unitCellAt {f : Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Torus.unitCell 2))) (hper : Torus.IsZdPeriodic f) (n : Fin 2 → ℤ) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Torus.unitCellAt 2 (Torus.intVector n)))

Periodic L² data have the same L² control on every integer translate of the unit cell.

theorem AVenhance.Infra.Heat.integral_periodic_heatPeriodicCutoff2 {g : Homogenization.Vec 2 → ℝ} (hper : Torus.IsZdPeriodic g) (hTile : ∀ (b : Bool × Bool), MeasureTheory.IntegrableOn g (heatPeriodicTile b) MeasureTheory.volume) : ∫ (x : Homogenization.Vec 2), g x * heatPeriodicCutoff2 x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x

A two-dimensional periodic integral unfolds through the product cutoff. The premise supplies the local integrability on the four translated cells.

theorem AVenhance.Infra.Heat.integral_periodic_weight2 {g w q : Homogenization.Vec 2 → ℝ} (hper : Torus.IsZdPeriodic g) (hSupport : Function.support w ⊆ ⋃ (b : Bool × Bool), heatPeriodicTile b) (hTile : ∀ (b : Bool × Bool), MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => g x * w x) (heatPeriodicTile b) MeasureTheory.volume) (hPeriod : ∀ x ∈ Torus.unitCell 2, ∑ b : Bool × Bool, w (x + heatPeriodicTileStart b) = q x) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => g x * w x) MeasureTheory.volume ∧ ∫ (x : Homogenization.Vec 2), g x * w x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x * q x

Folding against a compactly supported weight sums its translates over one unit cell. The tilewise integrability premise is convenient for weights such as derivatives of the partition cutoff.