Fourier coefficients of periodic weak gradients.

noncomputable def AVenhance.Infra.Heat.WeakFourier.heatWeakRealCharacter (k : Frequency) (x : Homogenization.Vec 2) : ℝ

Real part of a periodic character used in the weak heat equation.

Equations

• AVenhance.Infra.Heat.WeakFourier.heatWeakRealCharacter k x = Complex.reCLM (AVenhance.Infra.Torus.torusCharacter k x)

noncomputable def AVenhance.Infra.Heat.WeakFourier.heatWeakImagCharacter (k : Frequency) (x : Homogenization.Vec 2) : ℝ

Imaginary part of a periodic character used in the weak heat equation.

Equations

• AVenhance.Infra.Heat.WeakFourier.heatWeakImagCharacter k x = Complex.imCLM (AVenhance.Infra.Torus.torusCharacter k x)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_torusCharacter_line_eq {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : Torus.torusCharacter k (i.insertNth t z) = (fourier (-k i)) ↑t * ∏ j : Fin n, (fourier (-k (i.succAbove j))) ↑(z j)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_torusCharacter_line_hasDerivAt {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : HasDerivAt (fun (s : ℝ) => Torus.torusCharacter k (i.insertNth s z)) (-2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k (i.insertNth t z)) t

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_coordDeriv_torusCharacter (i : Fin 2) (k : Frequency) (x : Homogenization.Vec 2) : Torus.coordDeriv i (Torus.torusCharacter k) x = -2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_coordDeriv_realCharacter (i : Fin 2) (k : Frequency) (x : Homogenization.Vec 2) : (fderiv ℝ (heatWeakRealCharacter k) x) (Homogenization.basisVec i) = (-2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k x).re

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_coordDeriv_imagCharacter (i : Fin 2) (k : Frequency) (x : Homogenization.Vec 2) : (fderiv ℝ (heatWeakImagCharacter k) x) (Homogenization.basisVec i) = (-2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k x).im

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realCharacter_contDiff (k : Frequency) : ContDiff ℝ (↑⊤) (heatWeakRealCharacter k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagCharacter_contDiff (k : Frequency) : ContDiff ℝ (↑⊤) (heatWeakImagCharacter k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realCharacter_periodic (k : Frequency) : Torus.IsZdPeriodic (heatWeakRealCharacter k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagCharacter_periodic (k : Frequency) : Torus.IsZdPeriodic (heatWeakImagCharacter k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realCharacterDeriv_periodic (i : Fin 2) (k : Frequency) : Torus.IsZdPeriodic fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakRealCharacter k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagCharacterDeriv_periodic (i : Fin 2) (k : Frequency) : Torus.IsZdPeriodic fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakImagCharacter k) x) (Homogenization.basisVec i)

noncomputable def AVenhance.Infra.Heat.WeakFourier.heatWeakRealTest (k : Frequency) : Homogenization.Vec 2 → ℝ

Real periodic character localized by the compactly supported heat cutoff.

Equations

• AVenhance.Infra.Heat.WeakFourier.heatWeakRealTest k x = AVenhance.Infra.Heat.heatPeriodicCutoff2 x * AVenhance.Infra.Heat.WeakFourier.heatWeakRealCharacter k x

noncomputable def AVenhance.Infra.Heat.WeakFourier.heatWeakImagTest (k : Frequency) : Homogenization.Vec 2 → ℝ

Imaginary periodic character localized by the compactly supported heat cutoff.

Equations

• AVenhance.Infra.Heat.WeakFourier.heatWeakImagTest k x = AVenhance.Infra.Heat.heatPeriodicCutoff2 x * AVenhance.Infra.Heat.WeakFourier.heatWeakImagCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTest_contDiff (k : Frequency) : ContDiff ℝ (↑⊤) (heatWeakRealTest k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTest_contDiff (k : Frequency) : ContDiff ℝ (↑⊤) (heatWeakImagTest k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTest_hasCompactSupport (k : Frequency) : HasCompactSupport (heatWeakRealTest k)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTest_hasCompactSupport (k : Frequency) : HasCompactSupport (heatWeakImagTest k)

theorem AVenhance.Infra.Heat.WeakFourier.fderiv_heatWeakRealTest (i : Fin 2) (k : Frequency) (x : Homogenization.Vec 2) : (fderiv ℝ (heatWeakRealTest k) x) (Homogenization.basisVec i) = heatPeriodicCutoff2 x * (fderiv ℝ (heatWeakRealCharacter k) x) (Homogenization.basisVec i) + heatWeakRealCharacter k x * (fderiv ℝ heatPeriodicCutoff2 x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.fderiv_heatWeakImagTest (i : Fin 2) (k : Frequency) (x : Homogenization.Vec 2) : (fderiv ℝ (heatWeakImagTest k) x) (Homogenization.basisVec i) = heatPeriodicCutoff2 x * (fderiv ℝ (heatWeakImagCharacter k) x) (Homogenization.basisVec i) + heatWeakImagCharacter k x * (fderiv ℝ heatPeriodicCutoff2 x) (Homogenization.basisVec i)

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

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

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTest_periodization (k : Frequency) {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, heatWeakRealTest k (x + heatPeriodicTileStart b) = heatWeakRealCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTest_periodization (k : Frequency) {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, heatWeakImagTest k (x + heatPeriodicTileStart b) = heatWeakImagCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTestDeriv_periodization (i : Fin 2) (k : Frequency) {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, (fderiv ℝ (heatWeakRealTest k) (x + heatPeriodicTileStart b)) (Homogenization.basisVec i) = (fderiv ℝ (heatWeakRealCharacter k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTestDeriv_periodization (i : Fin 2) (k : Frequency) {x : Homogenization.Vec 2} (hx : x ∈ Torus.unitCell 2) : ∑ b : Bool × Bool, (fderiv ℝ (heatWeakImagTest k) (x + heatPeriodicTileStart b)) (Homogenization.basisVec i) = (fderiv ℝ (heatWeakImagCharacter k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTest_support_subset_tiles (k : Frequency) : Function.support (heatWeakRealTest k) ⊆ ⋃ (b : Bool × Bool), heatPeriodicTile b

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTest_support_subset_tiles (k : Frequency) : Function.support (heatWeakImagTest k) ⊆ ⋃ (b : Bool × Bool), heatPeriodicTile b

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_continuous_fderiv_apply {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => (fderiv ℝ f x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTestDeriv_continuous (i : Fin 2) (k : Frequency) : Continuous fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakRealTest k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTestDeriv_continuous (i : Fin 2) (k : Frequency) : Continuous fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakImagTest k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realTestDeriv_hasCompactSupport (i : Fin 2) (k : Frequency) : HasCompactSupport fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakRealTest k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagTestDeriv_hasCompactSupport (i : Fin 2) (k : Frequency) : HasCompactSupport fun (x : Homogenization.Vec 2) => (fderiv ℝ (heatWeakImagTest k) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Heat.WeakFourier.volume_unitCellAt_ne_top (a : Fin 2 → ℝ) : MeasureTheory.volume (Torus.unitCellAt 2 a) ≠ ⊤

theorem AVenhance.Infra.Heat.WeakFourier.memLp_heatWeak_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Torus.unitCell 2))

theorem AVenhance.Infra.Heat.WeakFourier.integrableOn_periodic_heatWeak_tile {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hper : Torus.IsZdPeriodic f) (b : Bool × Bool) : MeasureTheory.IntegrableOn f (heatPeriodicTile b) MeasureTheory.volume

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_norm_bound_of_continuous_compact_support {w : Homogenization.Vec 2 → ℝ} (hwc : Continuous w) (hws : HasCompactSupport w) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖w x‖ ≤ C

theorem AVenhance.Infra.Heat.WeakFourier.integrableOn_mul_of_norm_bound {f w : Homogenization.Vec 2 → ℝ} {S : Set (Homogenization.Vec 2)} (hf : MeasureTheory.IntegrableOn f S MeasureTheory.volume) (hw : Continuous w) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Homogenization.Vec 2), ‖w x‖ ≤ C) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => f x * w x) S MeasureTheory.volume

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_tile_weight_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hper : Torus.IsZdPeriodic f) {w : Homogenization.Vec 2 → ℝ} (hwc : Continuous w) (hws : HasCompactSupport w) (b : Bool × Bool) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => f x * w x) (heatPeriodicTile b) MeasureTheory.volume

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_torusCharacter_norm (k : Frequency) (x : Homogenization.Vec 2) : ‖Torus.torusCharacter k x‖ = 1

theorem AVenhance.Infra.Heat.WeakFourier.integrableOn_heatWeak_character_mul_real {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hper : Torus.IsZdPeriodic f) (k : Frequency) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => Torus.torusCharacter k x * ↑(f x)) (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_gradientCoord_periodic {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hDu : Torus.IsZdPeriodic Du) (i : Fin 2) : Torus.IsZdPeriodic fun (x : Homogenization.Vec 2) => Du x i

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realCellIBP {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u x * (fderiv ℝ (heatWeakRealCharacter k) x) (Homogenization.basisVec i) = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Du x i * heatWeakRealCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagCellIBP {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u x * (fderiv ℝ (heatWeakImagCharacter k) x) (Homogenization.basisVec i) = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Du x i * heatWeakImagCharacter k x

noncomputable def AVenhance.Infra.Heat.WeakFourier.heatWeakGradientMultiplier (i : Fin 2) (k : Frequency) : ℂ

Fourier multiplier for differentiation in a spatial coordinate.

Equations

• AVenhance.Infra.Heat.WeakFourier.heatWeakGradientMultiplier i k = 2 * ↑Real.pi * Complex.I * ↑(k i)

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_realMultiplier_cell {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u x * (heatWeakGradientMultiplier i k * Torus.torusCharacter k x).re = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Du x i * heatWeakRealCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_imagMultiplier_cell {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u x * (heatWeakGradientMultiplier i k * Torus.torusCharacter k x).im = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Du x i * heatWeakImagCharacter k x

theorem AVenhance.Infra.Heat.WeakFourier.heatWeak_gradientFourierCoeff_eq {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : (heatWeakGradientMultiplier i k * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Torus.torusCharacter k x * ↑(u x)).re = (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Torus.torusCharacter k x * ↑(Du x i)).re ∧ (heatWeakGradientMultiplier i k * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Torus.torusCharacter k x * ↑(u x)).im = (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Torus.torusCharacter k x * ↑(Du x i)).im

theorem AVenhance.Infra.Heat.mFourierCoeff_frozenPeriodicH1GradientL2 {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) (k : Frequency) : UnitAddTorus.mFourierCoeff (↑↑(frozenPeriodicH1GradientL2 h i)) k = 2 * ↑Real.pi * Complex.I * ↑(k i) * UnitAddTorus.mFourierCoeff (↑↑(frozenPeriodicH1ValueL2 h)) k