Fourier coefficient bounds for the all-order Galerkin limits.

@[instance_reducible]

noncomputable def classicalSmoothFourierMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalSmoothFourierMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalSmoothFourierProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalSmoothFourierOneLeTwoFact : Fact (1 ≤ 2)

theorem AVenhance.Infra.Classical.classicalGalerkinWordLimitFourierCoeffPath_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ↑(Set.Icc 0 1)) (k : Fin 2 → ℤ), ‖(classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k) t‖ ≤ C

Every Fourier coefficient of a derivative limit is uniformly bounded in time by its L² bound.

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalScaledIntegerFrequencyWeight_summable : Summable fun (n : ℤ) => (1 + 2 * Real.pi * |↑n|) ^ (-2)

theorem AVenhance.Infra.Classical.classicalScaledTorusFrequencyWeight_summable : Summable fun (k : Fin 2 → ℤ) => (1 + 2 * Real.pi * |↑(k 0)|) ^ (-2) * (1 + 2 * Real.pi * |↑(k 1)|) ^ (-2)

noncomputable def AVenhance.Infra.Classical.classicalScaledTorusFrequencyWeight (k : Fin 2 → ℤ) : ℝ

Summable product weight controlling the two-dimensional Fourier tail.

Equations

• AVenhance.Infra.Classical.classicalScaledTorusFrequencyWeight k = (1 + 2 * Real.pi * |↑(k 0)|) ^ (-2) * (1 + 2 * Real.pi * |↑(k 1)|) ^ (-2)

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalScaledTorusFrequencyWeight_eq_inv (k : Fin 2 → ℤ) : classicalScaledTorusFrequencyWeight k = ((1 + 2 * Real.pi * |↑(k 0)|) ^ 2 * (1 + 2 * Real.pi * |↑(k 1)|) ^ 2)⁻¹

theorem AVenhance.Infra.Classical.classicalWeightedCoeff_frequencyPower_le (n : ℕ) (x y a C : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (ha : 0 ≤ a) (hweight : (1 + x) ^ (n + 2) * (1 + y) ^ (n + 2) * a ≤ C) : a * (x + y) ^ n ≤ C * ((1 + x) ^ (-2) * (1 + y) ^ (-2))

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalGalerkinFourierMode_contDiff (a : ℂ) (k : Fin 2 → ℤ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => a * Torus.torusCharacter (-k) x

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalGalerkinFourierMode_derivative_norm_le (a : ℂ) (k : Fin 2 → ℤ) (n : ℕ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => a * Torus.torusCharacter (-k) y) x‖ ≤ ‖a‖ * (2 * Real.pi * ∑ i : Fin 2, |↑(k i)|) ^ n

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalGalerkinFourierMode_derivative_weighted_bound (a : ℂ) (k : Fin 2 → ℤ) (n : ℕ) (x : Homogenization.Vec 2) (C : ℝ) (hC : (1 + 2 * Real.pi * |↑(k 0)|) ^ (n + 2) * (1 + 2 * Real.pi * |↑(k 1)|) ^ (n + 2) * ‖a‖ ≤ C) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => a * Torus.torusCharacter (-k) y) x‖ ≤ C * classicalScaledTorusFrequencyWeight k

noncomputable def AVenhance.Infra.Classical.classicalGalerkinWordFourierMultiplier (k : Fin 2 → ℤ) (w : List (Fin 2)) : ℂ

The multiplier associated with one ordered list of spatial derivatives.

Equations

• AVenhance.Infra.Classical.classicalGalerkinWordFourierMultiplier k w = (List.map (fun (i : Fin 2) => 2 * ↑Real.pi * Complex.I * ↑(k i)) w).prod

theorem AVenhance.Infra.Classical.classicalGalerkinWordLimitFourierCoeff_word (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (w : List (Fin 2)) (k : Fin 2 → ℤ) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k) t = classicalGalerkinWordFourierMultiplier k w * (classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per [] k) t

Fourier coefficients of the derivative limits satisfy the full ordered-word multiplier identity.

theorem AVenhance.Infra.Classical.classicalGalerkinWordFourierMultiplier_replicate_norm (k : Fin 2 → ℤ) (i : Fin 2) (p : ℕ) : ‖classicalGalerkinWordFourierMultiplier k (List.replicate p i)‖ = (2 * Real.pi * |↑(k i)|) ^ p

The norm of a repeated coordinate multiplier is the corresponding scalar frequency power.

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalMaxFrequencyCoefficientBound (p : ℕ) (x y a C₀ C₁ C₂ C₃ : ℝ) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hC₃ : 0 ≤ C₃) (h₀ : a ≤ C₀) (h₁ : x ^ p * a ≤ C₁) (h₂ : y ^ p * a ≤ C₂) (h₃ : x ^ p * y ^ p * a ≤ C₃) : max 1 x ^ p * max 1 y ^ p * a ≤ C₀ + C₁ + C₂ + C₃

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalOneAddFrequency_pow_le (p : ℕ) (x : ℝ) (hx : 0 ≤ x) : (1 + x) ^ p ≤ 2 ^ p * max 1 x ^ p

theorem AVenhance.Infra.Classical.GalerkinSmoothFourier.classicalWeightedFrequencyCoefficientBound (p : ℕ) (x y a C₀ C₁ C₂ C₃ : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (ha : 0 ≤ a) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hC₃ : 0 ≤ C₃) (h₀ : a ≤ C₀) (h₁ : x ^ p * a ≤ C₁) (h₂ : y ^ p * a ≤ C₂) (h₃ : x ^ p * y ^ p * a ≤ C₃) : (1 + x) ^ p * (1 + y) ^ p * a ≤ 2 ^ p * 2 ^ p * (C₀ + C₁ + C₂ + C₃)

theorem AVenhance.Infra.Classical.classicalGalerkinBaseFourierCoeff_weighted_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (p : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (k : Fin 2 → ℤ) (t : ↑(Set.Icc 0 1)), (1 + 2 * Real.pi * |↑(k 0)|) ^ p * (1 + 2 * Real.pi * |↑(k 1)|) ^ p * ‖(classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per [] k) t‖ ≤ C

Uniform derivative energy bounds give polynomial decay of the base Fourier coefficients in both coordinate directions.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFourierCoefficientBound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (n : ℕ) : ℝ

Bound on the Fourier coefficients of the classical Galerkin solution.

Equations

• AVenhance.Infra.Classical.classicalGalerkinFourierCoefficientBound φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per n = Classical.choose ⋯

theorem AVenhance.Infra.Classical.classicalGalerkinFourierCoefficientBound_nonneg (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (n : ℕ) : 0 ≤ classicalGalerkinFourierCoefficientBound φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per n

theorem AVenhance.Infra.Classical.classicalGalerkinFourierCoefficientBound_spec (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (n : ℕ) (k : Fin 2 → ℤ) (t : ↑(Set.Icc 0 1)) : (1 + 2 * Real.pi * |↑(k 0)|) ^ (n + 2) * (1 + 2 * Real.pi * |↑(k 1)|) ^ (n + 2) * ‖(classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per [] k) t‖ ≤ classicalGalerkinFourierCoefficientBound φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per n

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFourierSeriesTerm (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) (k : Fin 2 → ℤ) : C(UnitAddTorus (Fin 2), ℂ)

One Fourier term of the classical Galerkin solution series.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinFourierSeriesTerm_summable (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : Summable (classicalGalerkinFourierSeriesTerm φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFourierContinuousLimit (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : C(UnitAddTorus (Fin 2), ℂ)

Continuous torus-valued limit of the classical Galerkin Fourier series.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinSmoothLift (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : Homogenization.Vec 2 → ℂ

Smooth Euclidean periodic lift of the classical Galerkin limit.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothLift_contDiff (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : ContDiff ℝ (↑⊤) (classicalGalerkinSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)

theorem AVenhance.Infra.Classical.classicalGalerkinFourierContinuousLimit_toLp (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : (ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (classicalGalerkinFourierContinuousLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) = classicalRealToComplexTorusCLM ((classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per []) t)

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothLift_eq_continuousLimit (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) (x : Homogenization.Vec 2) : classicalGalerkinSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t x = (classicalGalerkinFourierContinuousLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) (Torus.toUnitTorus 2 x)

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothLift_periodic (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : IsZ2Periodic (classicalGalerkinSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)