Weak Bridge

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[instance_reducible]

noncomputable def heatWeakMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• heatWeakMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem heatWeakIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem heatWeakProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev AVenhance.Infra.Heat.HeatCell : Type

The subtype carrier for the half-open unit fundamental cell.

Equations

• AVenhance.Infra.Heat.HeatCell = { x : Homogenization.Vec 2 // x ∈ AVenhance.Infra.Torus.unitCell 2 }

theorem AVenhance.Infra.Heat.memLp_frozenCellTransfer {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : MeasureTheory.MemLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => ↑(f x)) 2 MeasureTheory.volume

Membership of the canonical cell transfer in torus L².

noncomputable def AVenhance.Infra.Heat.frozenCellToTorusL2 {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ↥(Torus.TorusL2 2)

Put a real function with the cell L² control into the torus L² space by using its values on the canonical half-open cell.

Equations

• AVenhance.Infra.Heat.frozenCellToTorusL2 hf = MeasureTheory.MemLp.toLp (AVenhance.Infra.Torus.periodicToTorus fun (x : Homogenization.Vec 2) => ↑(f x)) ⋯

noncomputable def AVenhance.Infra.Heat.frozenCellGradientToTorusL2 {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hDu : Homogenization.GradMemL2On unitCube Du) (i : Fin 2) : ↥(Torus.TorusL2 2)

Coordinate L² transfer of the weak gradient.

Equations

• AVenhance.Infra.Heat.frozenCellGradientToTorusL2 hDu i = AVenhance.Infra.Heat.frozenCellToTorusL2 ⋯

noncomputable def AVenhance.Infra.Heat.frozenPeriodicH1ValueL2 {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) : ↥(Torus.TorusL2 2)

Scalar torus L² carrier associated to periodic H¹ data.

Equations

• AVenhance.Infra.Heat.frozenPeriodicH1ValueL2 h = AVenhance.Infra.Heat.frozenCellToTorusL2 ⋯

noncomputable def AVenhance.Infra.Heat.frozenPeriodicH1GradientL2 {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (i : Fin 2) : ↥(Torus.TorusL2 2)

A coordinate of the weak gradient of periodic H¹ data, transferred to torus L².

Equations

• AVenhance.Infra.Heat.frozenPeriodicH1GradientL2 h i = AVenhance.Infra.Heat.frozenCellGradientToTorusL2 ⋯ i

theorem AVenhance.Infra.Heat.WeakBridge.normSq_memLpToLp_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (g : α → ℂ) (hg : MeasureTheory.MemLp g 2 μ) : ‖MeasureTheory.MemLp.toLp g hg‖ ^ 2 = ∫ (x : α), ‖g x‖ ^ 2 ∂μ

theorem AVenhance.Infra.Heat.normSq_frozenCellToTorusL2_eq {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ‖frozenCellToTorusL2 hf‖ ^ 2 = l2NormSq f

The torus norm of the cell transfer is exactly its cell L² integral.

theorem AVenhance.Infra.Heat.mFourierCoeff_frozenCellToTorusL2 {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (k : Frequency) : UnitAddTorus.mFourierCoeff (↑↑(frozenCellToTorusL2 hf)) k = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Torus.torusCharacter k x * ↑(f x)

Fourier coefficients of the cell transfer are the usual complex Fourier integrals over the unit cell.

theorem AVenhance.Infra.Heat.norm_heatTorusSmoothLift_multiIndexDerivative_le_frozenH1 {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) (α : Fin 2 → ℕ) : ‖(ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (heatDerivativeTorusContinuous hs (frozenPeriodicH1ValueL2 h) α)‖ ≤ ↑(multiIndexDegree α).factorial * (1 / √s) ^ multiIndexDegree α * √(l2NormSq f)

The classical derivative bound from item 2, stated for the IsPeriodicH1With scalar carrier.