Mathlib.Analysis.Fourier
Two groups of results.
Basic 3 core · 3 supporting Reusable real-line energies with Lebesgue measure. ★ weightedEnergy_two
Weighted inverse-Fourier energies
Reusable real-line energies with Lebesgue measure. The Fourier convention used by the
other modules is Mathlib's 𝓕⁻ G(v) = ∫ ξ, exp(2π i ξv) G(ξ), so its unweighted
Plancherel constant is one and its quadratic moment constant is (2π)⁻².
def energy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The ordinary squared L² energy of a complex-valued function on the real line is the Lebesgue integral of its squared modulus.
Definition (Lean source)
parameters
g :
ℝ → ℂ
def
energy g :
ℝ
given by
∫ v, ‖g v‖ ^ 2
def weightedEnergy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The weighted squared L² energy for a moment exponent and a complex-valued function on the real line is the Lebesgue integral weighted by the κ-th power of distance from zero.
Definition (Lean source)
parameters
κ :
ℝ
g :
ℝ → ℂ
def
weightedEnergy κ g :
ℝ
given by
∫ v, |v| ^ κ * ‖g v‖ ^ 2
theorem weightedEnergy_two reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
A complex-valued function on the real line has weighted energy at exponent two equal to its squared-distance weighted integral.
Formal statement
Proof (Lean source)
theorem weightedEnergy_two (g : ℝ → ℂ) :
weightedEnergy 2 g = ∫ v, v ^ 2 * ‖g v‖ ^ 2 := by
simp [weightedEnergy, sq_abs]
3 supporting declarations (lemmas, instances)
-
energy_nonnegtheorem — A complex-valued function on the real line has nonnegative ordinary squared L² energy.Proof (Lean source)
-
weightedEnergy_nonnegtheorem — A moment exponent and a complex-valued function on the real line have nonnegative weighted squared L² energy.Proof (Lean source)
theorem weightedEnergy_nonneg (κ : ℝ) (g : ℝ → ℂ) : 0 ≤ weightedEnergy κ g := integral_nonneg fun v => mul_nonneg (Real.rpow_nonneg (abs_nonneg v) κ) (sq_nonneg _) -
weightedEnergy_zerotheorem — A complex-valued function on the real line has weighted energy at exponent zero equal to its ordinary squared L² energy.Proof (Lean source)
theorem weightedEnergy_zero (g : ℝ → ℂ) : weightedEnergy 0 g = energy g := by simp [weightedEnergy, energy]
AngularFourier 15 core · 26 supporting This module defines the unitary angular-frequency Fourier integral on finite-dimensional real Euclidean space and proves its compatibility with Mathlib's L² transform. ★ angular_plancherel
Finite-dimensional angular Fourier transforms
This module defines the unitary angular-frequency Fourier integral on finite-dimensional real Euclidean space and proves its compatibility with Mathlib's L² transform. It records the exact dilation normalization, Euclidean-coordinate volume identities, and Plancherel without any compact-support or derivative assumption.
abbrev Space reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The Euclidean space with dimension and its canonical coordinates.
Definition (Lean source)
def angularPrefactor reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The angular unitary prefactor in dimension is the negative half-dimensional power of two pi.
Definition (Lean source)
def angularFourier reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The angular Fourier transform of a complex spatial function at a frequency is (2π)^(−p/2) times the integral over u of exp(−i·⟨w, u⟩)·G(u), where p is the dimension and ⟨w, u⟩ is the sum of coordinate products.
Definition (Lean source)
parameters
def
angularFourier G w :
ℂ
given by
def coordinateVector reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The canonical coordinate vector for coordinate has value one in that coordinate and zero in the others.
def coordinateDerivative reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The coordinate derivative of a scalar test function in a coordinate at a point is its real Fréchet derivative evaluated on the canonical coordinate vector.
Definition (Lean source)
def HasWeakCoordinateDerivative reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
Spatial weak differentiation of a function by a proposed derivative in one coordinate means integration by parts against every smooth compactly supported complex scalar test.
Definition (Lean source)
parameters
def
HasWeakCoordinateDerivative G D r :
Prop
given by
(∫ x, G x * coordinateDerivative φ r x) = -(∫ x, D x * φ x)
def updateCoordinate reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The coordinate update of a point changes one coordinate to a real value.
abbrev RemainingCoordinates reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The remaining-coordinate space omits one coordinate from a finite product.
def insertCoordinate reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
Coordinate insertion combines the omitted coordinate, the remaining values, and one real value into a Euclidean point.
Definition (Lean source)
def HasRealSliceIBP reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
Real slice integration by parts for a real function G and a family D of proposed coordinate derivatives means: for every coordinate r, every base point x, and every real function v that is differentiable everywhere with continuous derivative v′, the integral over real t of G(x with coordinate r set to t)·v′(t) equals minus the integral over t of D_r(x with coordinate r set to t)·v(t). The identity is required on every coordinate line (not only almost every one) and for every such test function, with no support or decay condition on v; integrals of non-integrable functions are read as zero.
Definition (Lean source)
parameters
def
HasRealSliceIBP G D :
Prop
given by
(∫ t : ℝ, G (updateCoordinate x r t) * v' t)
= -(∫ t : ℝ, D r (updateCoordinate x r t) * v t)
def complexify reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The complexification of a real spatial function is its pointwise inclusion into the complex numbers.
def l2Energy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The squared spatial energy of a function is the nonnegative Lebesgue integral of its squared norm.
Definition (Lean source)
def zeroEnergy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The zero-order angular energy of a function is the squared energy of its normalized angular Fourier integral.
Definition (Lean source)
def firstEnergy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
The first-order angular energy of a function weights its squared angular Fourier integral by one plus squared frequency divided by the dimension.
theorem angular_plancherel reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
An integrable and square-integrable spatial function has equal angular Fourier and spatial squared energies.
Formal statement
hypotheses
conclusion
zeroEnergy G = l2Energy G
Proof (Lean source)
theorem angular_plancherel (G : Space p → ℂ)
(hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) :
zeroEnergy G = l2Energy G := by
have hn := l2Energy_normalized_dilation (p := p) (𝓕 G)
calc
zeroEnergy G = l2Energy (fun w : Space p =>
angularPrefactor p • (𝓕 G) ((2 * pi)⁻¹ • w)) := by
unfold zeroEnergy
congr 1
exact funext (angularFourier_eq_mathlib G)
_ = l2Energy (𝓕 G) := hn
_ = l2Energy G := mathlib_integral_plancherel G hG1 hG2
26 supporting declarations (lemmas, instances)
-
norm_sq_eq_sum_coordinatestheorem — The squared Euclidean norm is the sum of squared real coordinates.Proof (Lean source)
theorem norm_sq_eq_sum_coordinates (x : Space p) : ‖x‖ ^ 2 = ∑ r, (x r) ^ 2 := by simpa using EuclideanSpace.real_norm_sq_eq x -
angularPrefactor_postheorem — The angular prefactor is strictly positive in every finite dimension.Proof (Lean source)
theorem angularPrefactor_pos (p : ℕ) : 0 < angularPrefactor p := by exact Real.rpow_pos_of_pos (by positivity) _ -
angularPrefactor_sq_mul_volumeFactortheorem — The squared prefactor cancels the angular dilation's volume factor exactly.Proof (Lean source)
theorem angularPrefactor_sq_mul_volumeFactor (p : ℕ) : angularPrefactor p ^ 2 * (2 * pi) ^ p = 1 := by unfold angularPrefactor have h : 0 < 2 * pi := by positivity rw [← Real.rpow_natCast, ← Real.rpow_mul h.le, ← Real.rpow_natCast, ← Real.rpow_add h] have he : -(p : ℝ) / 2 * (2 : ℝ) + (p : ℝ) = 0 := by ring norm_num only [Nat.cast_ofNat] at * rw [he, Real.rpow_zero] -
map_angularDilation_volumetheorem — Dividing frequency by two pi multiplies the pushed-forward volume by two pi to the dimension.hypothesesp :ℕProof (Lean source)
theorem map_angularDilation_volume (p : ℕ) : Measure.map (fun w : Space p => (2 * pi)⁻¹ • w) volume = ofReal ((2 * pi) ^ p) • volume := by rw [Measure.map_addHaar_smul volume (inv_ne_zero (by positivity))] simp only [Space, finrank_euclideanSpace, Fintype.card_fin, inv_pow, inv_inv] rw [abs_of_pos (pow_pos (by positivity : 0 < 2 * pi) p)] -
l2Energy_normalized_dilationtheorem — Normalized angular dilation preserves the squared energy of a complex function, even when its energy is infinite.Proof (Lean source)
theorem l2Energy_normalized_dilation (F : Space p → ℂ) : l2Energy (fun w => angularPrefactor p • F ((2 * pi)⁻¹ • w)) = l2Energy F := by have hd : MeasurableEmbedding (fun w : Space p => (2 * pi)⁻¹ • w) := measurableEmbedding_const_smul₀ (inv_ne_zero (by positivity)) unfold l2Energy simp_rw [norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, ENNReal.ofReal_mul (sq_nonneg _)] rw [lintegral_const_mul' _ _ ENNReal.ofReal_ne_top, ← hd.lintegral_map (fun x => ofReal (‖F x‖ ^ 2)), map_angularDilation_volume, lintegral_smul_measure] rw [smul_eq_mul, ← mul_assoc, ← ENNReal.ofReal_mul (sq_nonneg _), angularPrefactor_sq_mul_volumeFactor, ENNReal.ofReal_one, one_mul] -
angularFourier_eq_mathlibtheorem — The angular exponential integral equals Mathlib's two-pi Fourier integral at frequency divided by two pi, with precisely the unitary prefactor.hypothesesconclusionProof (Lean source)
theorem angularFourier_eq_mathlib (G : Space p → ℂ) (w : Space p) : angularFourier G w = angularPrefactor p • (𝓕 G) ((2 * Real.pi)⁻¹ • w) := by unfold angularFourier rw [Real.fourier_eq'] congr 1 apply integral_congr_ae filter_upwards [] with u congr 1 rw [inner_smul_right, PiLp.inner_apply] simp only [RCLike.inner_apply, conj_trivial] push_cast have hpi : (2 * Real.pi : ℝ) ≠ 0 := by positivity have hc : (2 * (Real.pi : ℂ)) ≠ 0 := by exact_mod_cast hpi congr 1 field_simp -
integral_coordinatestheorem — Integrating in Euclidean coordinates agrees exactly with product Lebesgue integration; the canonical coordinate conversion has Jacobian one. -
map_insertCoordinate_volumetheorem — Coordinate insertion sends the product of the remaining-coordinate Lebesgue measure and one-dimensional Lebesgue measure to Euclidean volume.hypothesesp :sharedℕr :Fin pconclusionMeasure.map (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) (volume.prod volume)Proof (Lean source)
theorem map_insertCoordinate_volume (r : Fin p) : Measure.map (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) (volume.prod volume) = (volume : Measure (Space p)) := by let : Unique {s : Fin p // ¬s ≠ r} := { default := ⟨r, by simp⟩ uniq := fun s => Subtype.ext (not_not.mp s.property) } have hs := (volume_preserving_piEquivPiSubtypeProd (fun _ : Fin p => ℝ) (fun s => s ≠ r)).symm have hu := (volume_preserving_piUnique (fun _ : {s : Fin p // ¬s ≠ r} => ℝ)).symm have hm := (PiLp.volume_preserving_toLp (Fin p)).comp (hs.comp ((MeasurePreserving.id volume).prod hu)) convert hm.map_eq using 1 congr 1 funext zt apply PiLp.ext intro s by_cases h : s = r · subst s simp [insertCoordinate, Function.comp_def, MeasurableEquiv.piEquivPiSubtypeProd, Equiv.piEquivPiSubtypeProd, MeasurableEquiv.piUnique, Equiv.piUnique] · simp [insertCoordinate, Function.comp_def, MeasurableEquiv.piEquivPiSubtypeProd, Equiv.piEquivPiSubtypeProd, h] -
integral_coordinate_slicestheorem — An integrable Euclidean function may be integrated one coordinate at a time with the exact product measure normalization.hypothesesconclusion(∫ x, F x) = ∫ z : RemainingCoordinates r, ∫ t : ℝ, F (insertCoordinate r z t)Proof (Lean source)
theorem integral_coordinate_slices (r : Fin p) (F : Space p → ℂ) (hF : Integrable F volume) : (∫ x, F x) = ∫ z : RemainingCoordinates r, ∫ t : ℝ, F (insertCoordinate r z t) := by have hm : Measurable (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) := by unfold insertCoordinate apply (WithLp.measurable_toLp 2 (Fin p → ℝ)).comp apply measurable_pi_lambda intro s split_ifs <;> fun_prop have hp : MeasurePreserving (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) (volume.prod volume) volume := ⟨hm, map_insertCoordinate_volume r⟩ rw [← hp.map_eq, integral_map hp.measurable.aemeasurable (hp.map_eq.symm ▸ hF.aestronglyMeasurable)] exact integral_prod _ (hp.integrable_comp_of_integrable hF) -
integrable_fourier_test_productstheorem — An integrable function and a Schwartz test have integrable products in both sides of the Fourier pairing.hypothesesconclusionconclusion 1Integrable (fun w => φ w * (𝓕 G) w) volumeconclusion 2Integrable (fun x => (𝓕 φ) x * G x) volumeProof (Lean source)
theorem integrable_fourier_test_products (G : Space p → ℂ) (hG : Integrable G volume) (φ : SchwartzMap (Space p) ℂ) : Integrable (fun w => φ w * (𝓕 G) w) volume ∧ Integrable (fun x => (𝓕 φ) x * G x) volume := by have hcont : Continuous (𝓕 G) := VectorFourier.fourierIntegral_continuous Real.continuous_fourierChar continuous_inner hG constructor · exact φ.integrable.mul_bdd hcont.aestronglyMeasurable (Filter.Eventually.of_forall fun w => VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ G w) · exact hG.bdd_mul (𝓕 φ).continuous.aestronglyMeasurable (Filter.Eventually.of_forall fun x => (𝓕 φ).norm_le_seminorm ℝ x) -
integral_fourier_pairingtheorem — The Fourier integral of an L1 function pairs with a Schwartz test by transferring the Fourier transform to the test function.hypothesesconclusion(∫ w, φ w * (𝓕 G) w) = ∫ x, (𝓕 φ) x * G xProof (Lean source)
theorem integral_fourier_pairing (G : Space p → ℂ) (hG : Integrable G volume) (φ : SchwartzMap (Space p) ℂ) : (∫ w, φ w * (𝓕 G) w) = ∫ x, (𝓕 φ) x * G x := by have h := VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ (Space p)) (μ := volume) (ν := volume) Real.continuous_fourierChar continuous_inner φ.integrable hG simpa using! h.symm -
l2_fourier_pairingtheorem — Mathlib's Fourier L2 isometry pairs with a Schwartz test by transferring the Fourier transform to that test.hypothesesconclusion(∫ w, φ w * (Lp.fourierTransformₗᵢ (Space p) ℂ (hG.toLp G)) w) = ∫ x, (𝓕 φ) x * G xProof (Lean source)
theorem l2_fourier_pairing (G : Space p → ℂ) (hG : MemLp G 2 volume) (φ : SchwartzMap (Space p) ℂ) : (∫ w, φ w * (Lp.fourierTransformₗᵢ (Space p) ℂ (hG.toLp G)) w) = ∫ x, (𝓕 φ) x * G x := by have h := congrArg (fun T : TemperedDistribution (Space p) ℂ => T φ) (Lp.fourier_toTemperedDistribution_eq (hG.toLp G)) simp only [TemperedDistribution.fourier_apply, Lp.toTemperedDistribution_apply, smul_eq_mul] at h change (∫ x, (𝓕 φ) x * (hG.toLp G) x) = (∫ w, φ w * (Lp.fourierTransformₗᵢ (Space p) ℂ (hG.toLp G)) w) at h rw [← h] apply integral_congr_ae filter_upwards [hG.coeFn_toLp] with x hx rw [hx] -
fourierIntegral_ae_L2theorem — For an L1 and L2 function, Mathlib's pointwise Fourier integral and the representative of its Fourier L2 isometry agree almost everywhere.hypothesesProof (Lean source)
theorem fourierIntegral_ae_L2 (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : (𝓕 G) =ᵐ[volume] (fun w => (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) w) := by have hcont : Continuous (𝓕 G) := VectorFourier.fourierIntegral_continuous Real.continuous_fourierChar continuous_inner hG1 apply ae_eq_of_integral_contDiff_smul_eq hcont.locallyIntegrable (Lp.memLp _ |>.locallyIntegrable (by norm_num)) intro g hg hs let φ : SchwartzMap (Space p) ℂ := (hs.comp_left (show Complex.ofRealCLM 0 = 0 from rfl)).toSchwartzMap (Complex.ofRealCLM.contDiff.comp hg) have h := (integral_fourier_pairing G hG1 φ).trans (l2_fourier_pairing G hG2 φ).symm change (∫ w, Complex.ofRealCLM (g w) * (𝓕 G) w) = (∫ w, Complex.ofRealCLM (g w) * (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) w) at h simpa only [Complex.ofRealCLM_apply, Complex.real_smul] using h -
mathlib_fourier_memLptheorem — The Fourier integral of an L1 and L2 function belongs to L2.hypothesesProof (Lean source)
theorem mathlib_fourier_memLp (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : MemLp (𝓕 G) 2 volume := by exact (memLp_congr_ae (fourierIntegral_ae_L2 G hG1 hG2)).2 (Lp.memLp _) -
mathlib_integral_planchereltheorem — Mathlib's Fourier integral preserves the nonnegative squared energy of an L1 and L2 function, with no support or derivative assumptions.hypothesesProof (Lean source)
theorem mathlib_integral_plancherel (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : l2Energy (𝓕 G) = l2Energy G := by have hn : eLpNorm (𝓕 G) 2 volume = eLpNorm G 2 volume := calc _ = eLpNorm (fun w => (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) w) 2 volume := eLpNorm_congr_ae (fourierIntegral_ae_L2 G hG1 hG2) _ = ‖𝓕 (hG2.toLp G)‖ₑ := (Lp.enorm_def _).symm _ = ‖hG2.toLp G‖ₑ := by simpa only [ofReal_norm] using congrArg ofReal (Lp.norm_fourier_eq (hG2.toLp G)) _ = eLpNorm G 2 volume := Lp.enorm_toLp hG2 have henergy (f : Space p → ℂ) : l2Energy f = eLpNorm f 2 volume ^ 2 := by simpa only [l2Energy, ENNReal.ofReal_pow (norm_nonneg _), ofReal_norm, ENNReal.rpow_two, NNReal.coe_ofNat, ENNReal.coe_ofNat] using (eLpNorm_nnreal_pow_eq_lintegral (f := f) (μ := volume) (p := 2) (by norm_num)).symm rw [henergy, henergy, hn] -
integrable_angular_kerneltheorem — Every frequency kernel times an L1 spatial function is Bochner integrable.hypothesesconclusionProof (Lean source)
theorem integrable_angular_kernel (G : Space p → ℂ) (hG : Integrable G volume) (w : Space p) : Integrable (fun u => exp (-I * ((∑ r, w r * u r : ℝ) : ℂ)) * G u) volume := by have hc : Continuous (fun u : Space p => exp (-I * ((∑ r, w r * u r : ℝ) : ℂ))) := by fun_prop exact hG.bdd_mul (c := 1) hc.aestronglyMeasurable (Filter.Eventually.of_forall fun u => by simp [Complex.norm_exp]) -
angularFourier_continuoustheorem — The angular Fourier integral of an L1 function is continuous.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem angularFourier_continuous (G : Space p → ℂ) (hG : Integrable G volume) : Continuous (angularFourier G) := by have hc : Continuous (𝓕 G) := VectorFourier.fourierIntegral_continuous Real.continuous_fourierChar continuous_inner hG have hd : Continuous (fun w : Space p => (2 * pi)⁻¹ • w) := by fun_prop have he : angularFourier G = (fun w => angularPrefactor p • (𝓕 G) ((2 * pi)⁻¹ • w)) := funext (angularFourier_eq_mathlib G) rw [he] exact (continuous_const (y := angularPrefactor p)).smul (hc.comp hd) -
angularFourier_measurabletheorem — The angular Fourier integral of an L1 function is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem angularFourier_measurable (G : Space p → ℂ) (hG : Integrable G volume) : Measurable (angularFourier G) := (angularFourier_continuous G hG).measurable -
angularFourier_ae_L2theorem — For an L1 and L2 spatial function, the angular integral agrees almost everywhere with the normalized frequency dilation of Mathlib's L2 transform.hypothesesconclusion=ᵐ[volume] (fun w => angularPrefactor p • (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) ((2 * pi)⁻¹ • w))Proof (Lean source)
theorem angularFourier_ae_L2 (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : angularFourier G =ᵐ[volume] (fun w => angularPrefactor p • (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) ((2 * pi)⁻¹ • w)) := by have hd : Measurable (fun w : Space p => (2 * pi)⁻¹ • w) := by fun_prop have he : (𝓕 G) =ᵐ[Measure.map (fun w : Space p => (2 * pi)⁻¹ • w) volume] (fun w => (Lp.fourierTransformₗᵢ (Space p) ℂ (hG2.toLp G)) w) := by rw [map_angularDilation_volume] exact Measure.ae_smul_measure (fourierIntegral_ae_L2 G hG1 hG2) _ have hpull := ae_of_ae_map hd.aemeasurable he filter_upwards [hpull] with w hw rw [angularFourier_eq_mathlib, hw] -
angular_plancherel_integraltheorem — Angular Plancherel is available directly as the equality of the two nonnegative Lebesgue integrals, for every L1 and L2 spatial function.hypothesesProof (Lean source)
theorem angular_plancherel_integral (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : (∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2)) = ∫⁻ x, ofReal (‖G x‖ ^ 2) := angular_plancherel G hG1 hG2 -
l2Energy_lt_top_of_memLptheorem — An L2 function has finite squared spatial energy.hypothesesconclusionl2Energy G < ⊤Proof (Lean source)
theorem l2Energy_lt_top_of_memLp {F : Type*} [NormedAddCommGroup F] (G : Space p → F) (hG : MemLp G 2 volume) : l2Energy G < ⊤ := by exact (hasFiniteIntegral_iff_ofReal (Filter.Eventually.of_forall fun x => sq_nonneg ‖G x‖)).1 (hG.integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)).hasFiniteIntegral -
angularFourier_memLptheorem — The angular Fourier integral of an L1 and L2 function belongs to L2.hypothesesconclusionProof (Lean source)
theorem angularFourier_memLp (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : MemLp (angularFourier G) 2 volume := by have hc := angularFourier_continuous G hG1 apply (memLp_two_iff_integrable_sq_norm hc.aestronglyMeasurable).2 refine ⟨hc.norm.pow 2 |>.aestronglyMeasurable, ?_⟩ apply (hasFiniteIntegral_iff_ofReal (Filter.Eventually.of_forall fun w => sq_nonneg ‖angularFourier G w‖)).2 change zeroEnergy G < ⊤ rw [angular_plancherel G hG1 hG2] exact l2Energy_lt_top_of_memLp G hG2 -
integrable_angular_norm_sqtheorem — The squared norm of the angular transform of an L1 and L2 function is an integrable real function.hypothesesconclusionIntegrable (fun w => ‖angularFourier G w‖ ^ 2) volumeProof (Lean source)
theorem integrable_angular_norm_sq (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : Integrable (fun w => ‖angularFourier G w‖ ^ 2) volume := by exact (angularFourier_memLp G hG1 hG2).integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0) -
zeroEnergy_lt_toptheorem — The zero-order angular energy of an L1 and L2 function is finite.hypothesesconclusionzeroEnergy G < ⊤Proof (Lean source)
theorem zeroEnergy_lt_top (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : zeroEnergy G < ⊤ := by rw [angular_plancherel G hG1 hG2] exact l2Energy_lt_top_of_memLp G hG2 -
zeroEnergy_le_ennrealtheorem — Every upper bound in the nonnegative extended reals on spatial squared energy also bounds zero-order angular Fourier energy exactly.hypothesesconclusionzeroEnergy G ≤ AProof (Lean source)
theorem zeroEnergy_le_ennreal (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (A : ℝ≥0∞) (hA : l2Energy G ≤ A) : zeroEnergy G ≤ A := by rw [angular_plancherel G hG1 hG2] exact hA -
zeroEnergy_letheorem — Every finite real upper bound on spatial squared energy also bounds zero-order angular Fourier energy exactly.Proof (Lean source)
theorem zeroEnergy_le (G : Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (A : ℝ) (hA : l2Energy G ≤ ofReal A) : zeroEnergy G ≤ ofReal A := by rw [angular_plancherel G hG1 hG2] exact hA
FourierEndpoints 2 core · 2 supporting This module works with ordinary integral transforms, including compact C¹ multipliers that are not Schwartz functions (the sixth box convolution has only finite smoothness). ★ inverse_energy_endpoints
Plancherel and the quadratic inverse-Fourier energy
This module works with ordinary integral transforms, including compact C¹ multipliers that are not Schwartz functions (the sixth box convolution has only finite smoothness). The caller may supply absolute integrability of the inverse transforms of G and G'. These are standard inversion hypotheses, not assumptions of either weighted inequality.
Primary Mathlib sources checked in round 1:
* FourierTransform.lean: VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip;
* Inversion.lean: Continuous.fourier_fourierInv_eq;
* FourierTransformDeriv.lean: Real.fourier_deriv.
Upstream source: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Analysis/Fourier
structure CompactInverseData reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
Admissible compact inverse-Fourier data for a complex frequency multiplier consist of one continuous frequency derivative, compact spectral support, an integrable inverse transform, and an integrable inverse transform of its derivative.
Definition (Lean source)
parameters
G :
ℝ → ℂ
assumes
regularity :
ContDiff ℝ 1 G
compactSupport :
integrable_inverse :
Integrable (𝓕⁻ G)
integrable_inverse_deriv :
Integrable (𝓕⁻ (deriv G))
theorem inverse_energy_endpoints reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
For a complex frequency multiplier G with admissible compact inverse-Fourier data, writing g for its inverse Fourier transform, |g|² and v²·|g(v)|² are integrable, the integral of |g|² equals the integral of |G|², and the integral of v²·|g(v)|² equals (2π)⁻² times the integral of |G′|².
Formal statement
hypotheses
G :
ℝ → ℂ
hG :
conclusion
conclusion 1
Integrable (fun v => ‖𝓕⁻ G v‖ ^ 2)
conclusion 2
Integrable (fun v => v ^ 2 * ‖𝓕⁻ G v‖ ^ 2)
conclusion 4
Proof (Lean source)
theorem inverse_energy_endpoints (G : ℝ → ℂ) (hG : CompactInverseData G) :
Integrable (fun v => ‖𝓕⁻ G v‖ ^ 2) ∧
Integrable (fun v => v ^ 2 * ‖𝓕⁻ G v‖ ^ 2) ∧
energy (𝓕⁻ G) = energy G ∧
weightedEnergy 2 (𝓕⁻ G) = (2 * pi)⁻¹ ^ 2 * energy (deriv G) := by
have hc := hG.regularity.continuous
have hdc := hG.regularity.continuous_deriv (by simp)
have hi : Integrable G := hc.integrable_of_hasCompactSupport hG.compactSupport
have hdi : Integrable (deriv G) := hdc.integrable_of_hasCompactSupport hG.compactSupport.deriv
have hd := hG.regularity.differentiable (by simp)
obtain ⟨_, hs, he⟩ := inverse_plancherel G hc hi hG.integrable_inverse
obtain ⟨_, hds, hde⟩ := inverse_plancherel (deriv G) hdc hdi
hG.integrable_inverse_deriv
have hpi : (2 * pi) ≠ 0 := ne_of_gt (by positivity)
have hmoment (v : ℝ) :
v ^ 2 * ‖𝓕⁻ G v‖ ^ 2 =
(2 * pi)⁻¹ ^ 2 * ‖𝓕⁻ (deriv G) v‖ ^ 2 := by
rw [inverse_deriv_eq G hi hd hdi]
simp only [norm_mul, norm_neg, Complex.norm_ofNat, Complex.norm_real,
Real.norm_eq_abs, abs_of_pos Real.pi_pos, Complex.norm_I, mul_one]
rw [mul_pow, mul_pow, mul_pow, sq_abs]
field_simp
have hm : Integrable (fun v => v ^ 2 * ‖𝓕⁻ G v‖ ^ 2) := by
simp_rw [hmoment]
exact hds.const_mul _
refine ⟨hs, hm, he, ?_⟩
rw [weightedEnergy_two]
simp_rw [hmoment]
rw [integral_const_mul, ← energy, hde]
2 supporting declarations (lemmas, instances)
-
inverse_planchereltheorem — A continuous complex frequency function with an integrable frequency representation and an integrable inverse Fourier transform has equal finite squared L² energies in frequency and physical space.hypothesesconclusionconclusion 1Integrable (fun ξ => ‖G ξ‖ ^ 2)conclusion 2Integrable (fun v => ‖𝓕⁻ G v‖ ^ 2)Proof (Lean source)
theorem inverse_plancherel (G : ℝ → ℂ) (hcont : Continuous G) (hG : Integrable G) (hinv : Integrable (𝓕⁻ G)) : Integrable (fun ξ => ‖G ξ‖ ^ 2) ∧ Integrable (fun v => ‖𝓕⁻ G v‖ ^ 2) ∧ energy (𝓕⁻ G) = energy G := by have hforward : Integrable (𝓕 G) := by simpa only [Real.fourierInv_eq_fourier_neg, neg_neg] using hinv.comp_neg have hinversion := hcont.fourier_fourierInv_eq hG hforward have square_integrable (f : ℝ → ℂ) (hf : Integrable f) (C : ℝ) (hbound : ∀ x, ‖f x‖ ≤ C) : Integrable (fun x => ‖f x‖ ^ 2) := by apply (hf.norm.const_mul C).mono' (hf.aestronglyMeasurable.norm.pow 2) filter_upwards [] with x rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), pow_two] exact mul_le_mul_of_nonneg_right (hbound x) (norm_nonneg _) have hsqinv : Integrable (fun x => ‖𝓕⁻ G x‖ ^ 2) := square_integrable _ hinv (∫ x, ‖G x‖) fun x => VectorFourier.norm_fourierIntegral_le_integral_norm Real.fourierChar volume (-innerₗ ℝ) G x have hsqG : Integrable (fun x => ‖G x‖ ^ 2) := by apply square_integrable _ hG (∫ x, ‖𝓕⁻ G x‖) intro x rw [← congrFun hinversion x] exact VectorFourier.norm_fourierIntegral_le_integral_norm Real.fourierChar volume (innerₗ ℝ) (𝓕⁻ G) x refine ⟨hsqG, hsqinv, ?_⟩ have hflip : -(-innerₗ ℝ).flip = innerₗ ℝ := by ext simp have hsesq := VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip (innerSL ℂ) Real.continuous_fourierChar (show Continuous (fun p : ℝ × ℝ => (-innerₗ ℝ) p.1 p.2) from (innerSL ℝ).continuous₂.neg) hG hinv rw [hflip] at hsesq change (∫ x, inner ℂ (𝓕⁻ G x) (𝓕⁻ G x)) = ∫ x, inner ℂ (G x) (𝓕 (𝓕⁻ G) x) at hsesq rw [hinversion] at hsesq simp only [inner_self_eq_norm_sq_to_K] at hsesq exact_mod_cast hsesq -
inverse_deriv_eqtheorem — A complex frequency multiplier with an integrable frequency representation, a differentiable frequency profile, an integrable first derivative, and a physical-space location has the stated inverse-Fourier derivative–multiplication identity.hypothesesProof (Lean source)
theorem inverse_deriv_eq (G : ℝ → ℂ) (hG : Integrable G) (hdiff : Differentiable ℝ G) (hD : Integrable (deriv G)) (v : ℝ) : 𝓕⁻ (deriv G) v = (-2 * (Real.pi : ℂ) * I * (v : ℂ)) * 𝓕⁻ G v := by rw [Real.fourierInv_eq_fourier_neg, Real.fourierInv_eq_fourier_neg] simpa [smul_eq_mul, mul_neg, neg_mul] using congrFun (Real.fourier_deriv hG hdiff hD) (-v)
MultiplierBounds 2 core · 3 supporting For a bandwidth h, a sixth convolution of sinc frequency boxes is supported in [-3/(πh), 3/(πh)]. ★ inverseGaussian_deriv_energy_le
Quantitative inverse Gaussian multiplier bounds
For a bandwidth h, a sixth convolution of sinc frequency boxes is supported in
[-3/(πh), 3/(πh)]. Bounds ‖F‖∞ ≤ a h and ‖F'‖∞ ≤ b h² are the reusable
inputs; this module does not construct that convolution. On its support the inverse
Gaussian factor is at most exp(18 (σ/h)²). Squared norms therefore cost
exp(36 (σ/h)²). Integrating the support length gives fully visible L² constants.
def inverseGaussian reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
A Gaussian scale parameter and a complex frequency profile determine the inverse-Gaussian frequency multiplier by multiplication with the reciprocal Gaussian characteristic function.
theorem inverseGaussian_deriv_energy_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
For a complex frequency profile F with one continuous derivative, a nonnegative Gaussian scale σ and positive bandwidth h, and nonnegative height constants a and b, suppose F vanishes outside the interval of radius 3/(πh) around zero and |F| ≤ a·h and |F′| ≤ b·h² everywhere. Then the integral of the squared modulus of the derivative of the inverse-Gaussian multiplier of F is at most (6/π)·(b + 12π·a)²·h³·(1 + σ/h)⁴·exp(36·(σ/h)²).
Formal statement
hypotheses
F :
ℝ → ℂ
σ h a b :
ℝ
hF :
ContDiff ℝ 1 F
hh :
0 < h
hσ :
0 ≤ σ
ha :
0 ≤ a
hb :
0 ≤ b
hbound :
∀ ξ, ‖F ξ‖ ≤ a * h
hderiv :
∀ ξ, ‖deriv F ξ‖ ≤ b * h ^ 2
Proof (Lean source)
theorem inverseGaussian_deriv_energy_le (F : ℝ → ℂ) (σ h a b : ℝ)
(hF : ContDiff ℝ 1 F) (hh : 0 < h) (hσ : 0 ≤ σ) (ha : 0 ≤ a) (hb : 0 ≤ b)
(hsupport : support F ⊆ Icc (-(3 / (pi * h))) (3 / (pi * h)))
(hbound : ∀ ξ, ‖F ξ‖ ≤ a * h) (hderiv : ∀ ξ, ‖deriv F ξ‖ ≤ b * h ^ 2) :
energy (deriv (inverseGaussian σ F)) ≤
(6 / pi) * (b + 12 * pi * a) ^ 2 * h ^ 3 *
(1 + σ / h) ^ 4 * exp (36 * (σ / h) ^ 2) := by
have hG := inverseGaussian_contDiff F σ hF
have hsG : support (inverseGaussian σ F) ⊆
Icc (-(3 / (pi * h))) (3 / (pi * h)) := by
intro x hx
apply hsupport
contrapose! hx
simp [Function.mem_support, inverseGaussian, Function.notMem_support.mp hx]
have hsD : support (deriv (inverseGaussian σ F)) ⊆
Icc (-(3 / (pi * h))) (3 / (pi * h)) :=
support_deriv_subset.trans (closure_minimal hsG isClosed_Icc)
have ht : 0 ≤ σ / h := div_nonneg hσ hh.le
have hc : 0 ≤ b + 12 * pi * a := by positivity
have hpoly : b + 12 * pi * a * (σ / h) ^ 2 ≤
(b + 12 * pi * a) * (1 + σ / h) ^ 2 := by
have ht1 : 1 ≤ (1 + σ / h) ^ 2 := by nlinarith
have ht2 : (σ / h) ^ 2 ≤ (1 + σ / h) ^ 2 := by nlinarith
have h1 := mul_le_mul_of_nonneg_left ht1 hb
have h2 := mul_le_mul_of_nonneg_left ht2
(show 0 ≤ 12 * pi * a by positivity)
nlinarith only [h1, h2]
have hm : ∀ x ∈ Icc (-(3 / (pi * h))) (3 / (pi * h)),
‖deriv (inverseGaussian σ F) x‖ ≤
(h ^ 2 * (b + 12 * pi * a) * (1 + σ / h) ^ 2) *
exp (18 * (σ / h) ^ 2) := by
intro x hx
have hlog : |4 * pi ^ 2 * σ ^ 2 * x| ≤ 12 * pi * σ ^ 2 / h := by
rw [abs_mul, abs_of_nonneg (by positivity : 0 ≤ 4 * pi ^ 2 * σ ^ 2)]
calc
_ ≤ (4 * pi ^ 2 * σ ^ 2) * (3 / (pi * h)) :=
mul_le_mul_of_nonneg_left (abs_le.mpr hx) (by positivity)
_ = _ := by field_simp; ring
rw [inverseGaussian_deriv F σ x ((hF.differentiable (by norm_num)) x)]
simp only [norm_mul, Complex.norm_real, Real.norm_eq_abs,
abs_of_pos (Real.exp_pos _)]
have hsum : ‖deriv F x + F x * (4 * pi ^ 2 * σ ^ 2 * x : ℝ)‖ ≤
h ^ 2 * (b + 12 * pi * a * (σ / h) ^ 2) := by
calc
_ ≤ ‖deriv F x‖ + ‖F x * (4 * pi ^ 2 * σ ^ 2 * x : ℝ)‖ := norm_add_le _ _
_ ≤ b * h ^ 2 + (a * h) * (12 * pi * σ ^ 2 / h) := by
rw [norm_mul, Complex.norm_real, Real.norm_eq_abs]
exact add_le_add (hderiv x) (mul_le_mul (hbound x) hlog (abs_nonneg _) (by positivity))
_ = _ := by field_simp
calc
_ ≤ (h ^ 2 * (b + 12 * pi * a * (σ / h) ^ 2)) *
exp (18 * (σ / h) ^ 2) :=
mul_le_mul hsum (Real.exp_le_exp.mpr (gaussian_exponent_le σ h x hh hx))
(by positivity) (by positivity)
_ ≤ _ := mul_le_mul_of_nonneg_right
(by nlinarith [mul_le_mul_of_nonneg_left hpoly (sq_nonneg h)]) (by positivity)
have he := energy_le_interval (deriv (inverseGaussian σ F)) (3 / (pi * h))
((h ^ 2 * (b + 12 * pi * a) * (1 + σ / h) ^ 2) *
exp (18 * (σ / h) ^ 2)) (hG.continuous_deriv (by norm_num))
(by positivity) hsD hm
calc
_ ≤ _ := he
_ = _ := by
rw [mul_pow, ← Real.exp_nat_mul]
norm_num only [Nat.cast_ofNat]
have hex : (2 : ℝ) * (18 * (σ / h) ^ 2) = 36 * (σ / h) ^ 2 := by ring
rw [hex]
field_simp
ring
3 supporting declarations (lemmas, instances)
-
inverseGaussian_contDifftheorem — A complex frequency profile with one continuous derivative and a Gaussian scale parameter give an inverse-Gaussian multiplier with one continuous derivative.Proof (Lean source)
theorem inverseGaussian_contDiff (F : ℝ → ℂ) (σ : ℝ) (hF : ContDiff ℝ 1 F) : ContDiff ℝ 1 (inverseGaussian σ F) := by unfold inverseGaussian apply hF.mul exact Complex.ofRealCLM.contDiff.comp (Real.contDiff_exp.comp ((contDiff_const.mul ((contDiff_const.mul contDiff_id).pow 2)).div_const 2)) -
inverseGaussian_hasCompactSupporttheorem — A complex frequency profile with compact spectral support and a Gaussian scale parameter give an inverse-Gaussian multiplier with compact spectral support.hypothesesconclusionProof (Lean source)
theorem inverseGaussian_hasCompactSupport (F : ℝ → ℂ) (σ : ℝ) (hF : HasCompactSupport F) : HasCompactSupport (inverseGaussian σ F) := by exact hF.mul_right -
inverseGaussian_energy_letheorem — A continuous complex frequency profile, a Gaussian scale parameter and positive bandwidth, a nonnegative height constant, sinc-six spectral support, and a uniform height bound imply the stated squared L² bound for the inverse-Gaussian multiplier.hypothesesF :ℝ → ℂσ h a :ℝhF :hh :0 < hha :0 ≤ ahbound :∀ ξ, ‖F ξ‖ ≤ a * hconclusionProof (Lean source)
theorem inverseGaussian_energy_le (F : ℝ → ℂ) (σ h a : ℝ) (hF : Continuous F) (hh : 0 < h) (ha : 0 ≤ a) (hsupport : support F ⊆ Icc (-(3 / (pi * h))) (3 / (pi * h))) (hbound : ∀ ξ, ‖F ξ‖ ≤ a * h) : energy (inverseGaussian σ F) ≤ (6 / pi) * a ^ 2 * h * exp (36 * (σ / h) ^ 2) := by have hs : support (inverseGaussian σ F) ⊆ Icc (-(3 / (pi * h))) (3 / (pi * h)) := by intro x hx apply hsupport contrapose! hx simp [Function.mem_support, inverseGaussian, Function.notMem_support.mp hx] have hg : Continuous (inverseGaussian σ F) := by unfold inverseGaussian fun_prop have hm : ∀ x ∈ Icc (-(3 / (pi * h))) (3 / (pi * h)), ‖inverseGaussian σ F x‖ ≤ a * h * exp (18 * (σ / h) ^ 2) := by intro x hx simp only [inverseGaussian, norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] exact mul_le_mul (hbound x) (Real.exp_le_exp.mpr (gaussian_exponent_le σ h x hh hx)) (le_of_lt (Real.exp_pos _)) (mul_nonneg ha hh.le) have he := energy_le_interval (inverseGaussian σ F) (3 / (pi * h)) (a * h * exp (18 * (σ / h) ^ 2)) hg (by positivity) hs hm calc _ ≤ _ := he _ = _ := by rw [mul_pow, ← Real.exp_nat_mul] have hex : (2 : ℝ) * (18 * (σ / h) ^ 2) = 36 * (σ / h) ^ 2 := by ring norm_num only [Nat.cast_ofNat] at * rw [hex] field_simp ring
AngularFourierSobolev 1 core · 15 supporting This module combines angular Plancherel with weak coordinate multipliers to identify the zero- and first-order Fourier energies of compactly supported functions. ★ angular_first_energy
Angular Fourier Sobolev energies
This module combines angular Plancherel with weak coordinate multipliers to identify the zero- and first-order Fourier energies of compactly supported functions. It includes the real slice interface, finite energy bounds, and exact dimension-two specializations.
theorem angular_first_energy reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
In a positive dimension p, for an integrable, square-integrable, compactly supported complex function G whose weak coordinate derivatives D_r are integrable and square-integrable, the first-order angular Fourier energy of G — the integral of |Ĝ(w)|²·(1 + ‖w‖²/p) — equals the squared L² energy of G plus 1/p times the sum over coordinates of the squared L² energies of the D_r.
Formal statement
hypotheses
p :
ℕ
hp :
1 ≤ p
G :
Space p → ℂ
hG1 :
hGc :
hD1 :
∀ r, Integrable (D r) volume
hweak :
∀ r, HasWeakCoordinateDerivative G (D r) r
conclusion
Proof (Lean source)
theorem angular_first_energy (hp : 1 ≤ p) (G : Space p → ℂ)
(D : Fin p → Space p → ℂ)
(hG1 : Integrable G volume) (hG2 : MemLp G 2 volume)
(hGc : HasCompactSupport G)
(hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume)
(hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) :
firstEnergy G = l2Energy G + ofReal ((p : ℝ)⁻¹) *
∑ r, l2Energy (D r) := by
rw [firstEnergy_eq_coordinate_sum hp G hG1, angular_plancherel G hG1 hG2]
have hc : ∀ r : Fin p,
(∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2 * (w r) ^ 2)) =
l2Energy (D r) := fun r =>
angular_coordinate_energy G (D r) r (hD1 r) (hD2 r) hGc (hweak r)
simp_rw [hc]
15 supporting declarations (lemmas, instances)
-
firstEnergy_density_measurabletheorem — The first-order angular density of an L1 function is a nonnegative measurable real function.hypothesesconclusionMeasurable (fun w => ‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ)))Proof (Lean source)
@[fun_prop] theorem firstEnergy_density_measurable (G : Space p → ℂ) (hG : Integrable G volume) : Measurable (fun w => ‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ))) := by have hF := angularFourier_measurable G hG fun_prop -
angular_coordinate_energytheorem — A coordinate-weighted squared Fourier energy equals the spatial squared energy of the corresponding L1 and L2 weak derivative.Proof (Lean source)
theorem angular_coordinate_energy (G D : Space p → ℂ) (r : Fin p) (hD1 : Integrable D volume) (hD2 : MemLp D 2 volume) (hGc : HasCompactSupport G) (hweak : HasWeakCoordinateDerivative G D r) : (∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2 * (w r) ^ 2)) = l2Energy D := by calc _ = zeroEnergy D := by apply lintegral_congr intro w congr 1 rw [angularFourier_weakDerivative G D r hD1 hGc hweak w] simp only [norm_mul, Complex.norm_I, Complex.norm_real, one_mul, mul_pow, Real.norm_eq_abs, sq_abs] ring _ = l2Energy D := angular_plancherel D hD1 hD2 -
firstEnergy_eq_coordinate_sumtheorem — The first-order angular energy splits into zero-order energy plus the dimensionally averaged sum of coordinate-weighted energies, including infinite energies; only L1 and positive dimension are needed for this splitting.hypothesesconclusion= zeroEnergy GProof (Lean source)
theorem firstEnergy_eq_coordinate_sum (hp : 1 ≤ p) (G : Space p → ℂ) (hG : Integrable G volume) : firstEnergy G = zeroEnergy G + ofReal ((p : ℝ)⁻¹) * ∑ r : Fin p, ∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2 * (w r) ^ 2) := by classical have hF := angularFourier_measurable G hG have hzero : Measurable (fun w => ofReal (‖angularFourier G w‖ ^ 2)) := by fun_prop have hcoord (r : Fin p) : Measurable (fun w : Space p => ofReal (‖angularFourier G w‖ ^ 2 * (w r) ^ 2)) := by fun_prop have hdensity (w : Space p) : ‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ)) = ‖angularFourier G w‖ ^ 2 + (p : ℝ)⁻¹ * ∑ r : Fin p, ‖angularFourier G w‖ ^ 2 * (w r) ^ 2 := by rw [norm_sq_eq_sum_coordinates, ← Finset.mul_sum] ring have henn (w : Space p) : ofReal (‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ))) = ofReal (‖angularFourier G w‖ ^ 2) + ofReal ((p : ℝ)⁻¹) * ∑ r : Fin p, ofReal (‖angularFourier G w‖ ^ 2 * (w r) ^ 2) := by rw [hdensity, ENNReal.ofReal_add (sq_nonneg _) (by positivity), ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_sum_of_nonneg (fun r _ => mul_nonneg (sq_nonneg _) (sq_nonneg _))] unfold firstEnergy zeroEnergy l2Energy simp_rw [henn] rw [lintegral_add_left hzero, lintegral_const_mul' _ _ ENNReal.ofReal_ne_top, lintegral_finsetSum univ (fun r _ => hcoord r)] -
angular_first_energy_integraltheorem — The exact first-order identity is also available as a literal nonnegative integral equality with the angular frequency weight.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rProof (Lean source)
theorem angular_first_energy_integral (hp : 1 ≤ p) (G : Space p → ℂ) (D : Fin p → Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) : (∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ)))) = (∫⁻ x, ofReal (‖G x‖ ^ 2)) + ofReal ((p : ℝ)⁻¹) * ∑ r, ∫⁻ x, ofReal (‖D r x‖ ^ 2) := angular_first_energy hp G D hG1 hG2 hGc hD1 hD2 hweak -
firstEnergy_lt_toptheorem — Under the spatial weak-derivative hypotheses, the first-order angular Fourier energy is finite.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rconclusionfirstEnergy G < ⊤Proof (Lean source)
theorem firstEnergy_lt_top (hp : 1 ≤ p) (G : Space p → ℂ) (D : Fin p → Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) : firstEnergy G < ⊤ := by rw [angular_first_energy hp G D hG1 hG2 hGc hD1 hD2 hweak] exact ENNReal.add_lt_top.mpr ⟨l2Energy_lt_top_of_memLp G hG2, ENNReal.mul_lt_top ENNReal.ofReal_lt_top (ENNReal.sum_lt_top.mpr fun r _ => l2Energy_lt_top_of_memLp (D r) (hD2 r))⟩ -
integrable_firstEnergy_densitytheorem — Under the spatial weak-derivative hypotheses, the weighted squared angular Fourier norm is Bochner integrable as a real function.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rconclusionIntegrable (fun w => ‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ))) volumeProof (Lean source)
theorem integrable_firstEnergy_density (hp : 1 ≤ p) (G : Space p → ℂ) (D : Fin p → Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) : Integrable (fun w => ‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / (p : ℝ))) volume := by refine ⟨(firstEnergy_density_measurable G hG1).aestronglyMeasurable, ?_⟩ apply (hasFiniteIntegral_iff_ofReal (Filter.Eventually.of_forall fun w => mul_nonneg (sq_nonneg _) (add_nonneg zero_le_one (div_nonneg (sq_nonneg _) (Nat.cast_nonneg p))))).2 exact firstEnergy_lt_top hp G D hG1 hG2 hGc hD1 hD2 hweak -
firstEnergy_le_ennrealtheorem — Spatial energy bounds in the nonnegative extended reals give the exact upper bound A plus B divided by dimension for first-order angular Fourier energy.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rA B :ℝ≥0∞hA :l2Energy G ≤ AhB :(∑ r, l2Energy (D r)) ≤ BconclusionfirstEnergy G ≤ A + ofReal ((p : ℝ)⁻¹) * BProof (Lean source)
theorem firstEnergy_le_ennreal (hp : 1 ≤ p) (G : Space p → ℂ) (D : Fin p → Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) (A B : ℝ≥0∞) (hA : l2Energy G ≤ A) (hB : (∑ r, l2Energy (D r)) ≤ B) : firstEnergy G ≤ A + ofReal ((p : ℝ)⁻¹) * B := by rw [angular_first_energy hp G D hG1 hG2 hGc hD1 hD2 hweak] exact add_le_add hA (mul_le_mul_right hB _) -
firstEnergy_letheorem — Finite nonnegative real spatial energy bounds A and B give the exact upper bound A plus B divided by dimension for first-order angular Fourier energy.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rA B :ℝhA0 :0 ≤ AhB0 :0 ≤ BconclusionfirstEnergy G ≤ ofReal (A + (p : ℝ)⁻¹ * B)Proof (Lean source)
theorem firstEnergy_le (hp : 1 ≤ p) (G : Space p → ℂ) (D : Fin p → Space p → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) (A B : ℝ) (hA0 : 0 ≤ A) (hB0 : 0 ≤ B) (hA : l2Energy G ≤ ofReal A) (hB : (∑ r, l2Energy (D r)) ≤ ofReal B) : firstEnergy G ≤ ofReal (A + (p : ℝ)⁻¹ * B) := by have hb := firstEnergy_le_ennreal hp G D hG1 hG2 hGc hD1 hD2 hweak (ofReal A) (ofReal B) hA hB rw [← ENNReal.ofReal_mul (inv_nonneg.mpr (Nat.cast_nonneg p)), ← ENNReal.ofReal_add hA0 (mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg p)) hB0)] at hb exact hb -
angular_first_energy_of_real_slicestheorem — A real compactly supported L1 and L2 function with L1 and L2 proposed derivatives satisfying coordinate-slice integration by parts obeys the exact complexified angular energy identity.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℝhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehslice :HasRealSliceIBP G DconclusionProof (Lean source)
theorem angular_first_energy_of_real_slices (hp : 1 ≤ p) (G : Space p → ℝ) (D : Fin p → Space p → ℝ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hslice : HasRealSliceIBP G D) : firstEnergy (complexify G) = l2Energy G + ofReal ((p : ℝ)⁻¹) * ∑ r, l2Energy (D r) := by have h := angular_first_energy hp (complexify G) (fun r => complexify (D r)) (integrable_complexify G hG1) (memLp_complexify G hG2) (hasCompactSupport_complexify G hGc) (fun r => integrable_complexify (D r) (hD1 r)) (fun r => memLp_complexify (D r) (hD2 r)) (sliceIBP_to_weakDerivative G D hG1 hD1 hslice) simpa only [l2Energy_complexify] using h -
firstEnergy_lt_top_of_real_slicestheorem — The complexified first-order angular energy from real coordinate-slice integration by parts is finite.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℝhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehslice :HasRealSliceIBP G DconclusionfirstEnergy (complexify G) < ⊤Proof (Lean source)
theorem firstEnergy_lt_top_of_real_slices (hp : 1 ≤ p) (G : Space p → ℝ) (D : Fin p → Space p → ℝ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hslice : HasRealSliceIBP G D) : firstEnergy (complexify G) < ⊤ := by rw [angular_first_energy_of_real_slices hp G D hG1 hG2 hGc hD1 hD2 hslice] exact ENNReal.add_lt_top.mpr ⟨l2Energy_lt_top_of_memLp G hG2, ENNReal.mul_lt_top ENNReal.ofReal_lt_top (ENNReal.sum_lt_top.mpr fun r _ => l2Energy_lt_top_of_memLp (D r) (hD2 r))⟩ -
energy_bounds_of_real_slicestheorem — Spatial bounds for real slice data give simultaneous finite zero-order and first-order angular energy bounds, with the exact reciprocal dimension.hypothesesp :sharedℕhp :1 ≤ pG :Space p → ℝhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehslice :HasRealSliceIBP G DA B :ℝhA0 :0 ≤ AhB0 :0 ≤ Bconclusionconclusion 1conclusion 2Proof (Lean source)
theorem energy_bounds_of_real_slices (hp : 1 ≤ p) (G : Space p → ℝ) (D : Fin p → Space p → ℝ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hslice : HasRealSliceIBP G D) (A B : ℝ) (hA0 : 0 ≤ A) (hB0 : 0 ≤ B) (hA : l2Energy G ≤ ofReal A) (hB : (∑ r, l2Energy (D r)) ≤ ofReal B) : zeroEnergy (complexify G) ≤ ofReal A ∧ firstEnergy (complexify G) ≤ ofReal (A + (p : ℝ)⁻¹ * B) := by constructor · apply zeroEnergy_le (complexify G) (integrable_complexify G hG1) (memLp_complexify G hG2) A simpa only [l2Energy_complexify] using hA · apply firstEnergy_le hp (complexify G) (fun r => complexify (D r)) (integrable_complexify G hG1) (memLp_complexify G hG2) (hasCompactSupport_complexify G hGc) (fun r => integrable_complexify (D r) (hD1 r)) (fun r => memLp_complexify (D r) (hD2 r)) (sliceIBP_to_weakDerivative G D hG1 hD1 hslice) A B hA0 hB0 · simpa only [l2Energy_complexify] using hA · simpa only [l2Energy_complexify] using hB -
angular_plancherel_twotheorem — In dimension two, every L1 and L2 complex function has equal spatial and angular Fourier squared energies.hypothesesProof (Lean source)
theorem angular_plancherel_two (G : Space 2 → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) : (∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2)) = ∫⁻ x, ofReal (‖G x‖ ^ 2) := angular_plancherel G hG1 hG2 -
angular_first_energy_twotheorem — In dimension two, the first-order energy is exactly the spatial energy plus one half of the sum of the two weak derivative energies.hypothesesG :Space 2 → ℂhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehweak :∀ r, HasWeakCoordinateDerivative G (D r) rProof (Lean source)
theorem angular_first_energy_two (G : Space 2 → ℂ) (D : Fin 2 → Space 2 → ℂ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hweak : ∀ r, HasWeakCoordinateDerivative G (D r) r) : (∫⁻ w, ofReal (‖angularFourier G w‖ ^ 2 * (1 + ‖w‖ ^ 2 / 2))) = l2Energy G + ofReal (1 / 2 : ℝ) * (l2Energy (D 0) + l2Energy (D 1)) := by simpa [firstEnergy, Fin.sum_univ_two, one_div] using angular_first_energy (p := 2) (by decide) G D hG1 hG2 hGc hD1 hD2 hweak -
angular_first_energy_two_real_slicestheorem — In dimension two, real slice integration by parts supplies exactly the same energy identity, with the sum of the two real derivative energies.hypothesesconclusionProof (Lean source)
theorem angular_first_energy_two_real_slices (G : Space 2 → ℝ) (D : Fin 2 → Space 2 → ℝ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hslice : HasRealSliceIBP G D) : firstEnergy (complexify G) = l2Energy G + ofReal (1 / 2 : ℝ) * (l2Energy (D 0) + l2Energy (D 1)) := by simpa [Fin.sum_univ_two, one_div] using angular_first_energy_of_real_slices (p := 2) (by decide) G D hG1 hG2 hGc hD1 hD2 hslice -
energy_bounds_two_real_slicestheorem — In dimension two, spatial bounds A and B yield the exact angular upper bounds A and A plus one half B for real coordinate-slice data.hypothesesG :Space 2 → ℝhG1 :hGc :hD1 :∀ r, Integrable (D r) volumehslice :HasRealSliceIBP G DA B :ℝhA0 :0 ≤ AhB0 :0 ≤ Bconclusionconclusion 1conclusion 2Proof (Lean source)
theorem energy_bounds_two_real_slices (G : Space 2 → ℝ) (D : Fin 2 → Space 2 → ℝ) (hG1 : Integrable G volume) (hG2 : MemLp G 2 volume) (hGc : HasCompactSupport G) (hD1 : ∀ r, Integrable (D r) volume) (hD2 : ∀ r, MemLp (D r) 2 volume) (hslice : HasRealSliceIBP G D) (A B : ℝ) (hA0 : 0 ≤ A) (hB0 : 0 ≤ B) (hA : l2Energy G ≤ ofReal A) (hB : l2Energy (D 0) + l2Energy (D 1) ≤ ofReal B) : zeroEnergy (complexify G) ≤ ofReal A ∧ firstEnergy (complexify G) ≤ ofReal (A + (1 / 2 : ℝ) * B) := by have hB' : (∑ r, l2Energy (D r)) ≤ ofReal B := by simpa [Fin.sum_univ_two] using hB simpa [one_div] using energy_bounds_of_real_slices (p := 2) (by decide) G D hG1 hG2 hGc hD1 hD2 hslice A B hA0 hB0 hA hB'
AngularFourierWeakDerivative 1 core · 16 supporting This module supplies the spatial weak-derivative interface and proves the angular Fourier multiplier identity. ★ sliceIBP_to_weakDerivative
Weak coordinate derivatives for angular Fourier transforms
This module supplies the spatial weak-derivative interface and proves the angular Fourier multiplier identity. It also turns real coordinate-slice integration by parts into that interface using the exact Euclidean/product-Lebesgue coordinate equivalence.
theorem sliceIBP_to_weakDerivative reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
An integrable real spatial function and integrable proposed coordinate derivatives satisfying real slice integration by parts give in each coordinate the complex weak derivative: the complexified proposed derivative is the weak coordinate derivative of the complexified function.
Formal statement
hypotheses
p :
ℕ
G :
Space p → ℝ
hG :
hD :
∀ r, Integrable (D r) volume
hslice :
HasRealSliceIBP G D
r :
Fin p
conclusion
Proof (Lean source)
theorem sliceIBP_to_weakDerivative (G : Space p → ℝ) (D : Fin p → Space p → ℝ)
(hG : Integrable G volume) (hD : ∀ r, Integrable (D r) volume)
(hslice : HasRealSliceIBP G D) (r : Fin p) :
HasWeakCoordinateDerivative (complexify G) (complexify (D r)) r := by
intro φ hφ hφc
obtain ⟨hleft, hright⟩ := integrable_compact_test_products
(complexify G) (complexify (D r)) r (integrable_complexify G hG)
(integrable_complexify (D r) (hD r)) φ hφ hφc
have hupdate (z : RemainingCoordinates r) (t : ℝ) :
updateCoordinate (insertCoordinate r z 0) r t = insertCoordinate r z t := by
apply PiLp.ext
intro s
by_cases hs : s = r
· subst s
simp [updateCoordinate, insertCoordinate]
· simp [updateCoordinate, insertCoordinate, hs]
rw [integral_coordinate_slices r _ hleft, integral_coordinate_slices r _ hright,
← integral_neg]
apply integral_congr_ae
filter_upwards [integrable_coordinate_slices_ae _ hleft r,
integrable_coordinate_slices_ae _ hright r] with z hzleft hzright
have h := realSliceIBP_complex_test G D hslice r (insertCoordinate r z 0)
(fun t => φ (updateCoordinate (insertCoordinate r z 0) r t))
(fun t => coordinateDerivative φ r (updateCoordinate (insertCoordinate r z 0) r t))
(hasDerivAt_test_coordinate_slice φ hφ (insertCoordinate r z 0) r)
(continuous_test_coordinate_slice_derivative φ hφ (insertCoordinate r z 0) r)
(by simpa only [hupdate, complexify] using hzleft)
(by simpa only [hupdate, complexify] using hzright)
simpa only [hupdate, complexify] using h
16 supporting declarations (lemmas, instances)
-
weakDerivative_zero_off_supporttheorem — An integrable weak coordinate derivative of a function vanishes almost everywhere outside the topological support of that function.hypothesesconclusion∀ᵐ x ∂volume, x ∉ tsupport G → D x = 0Proof (Lean source)
theorem weakDerivative_zero_off_support (G D : Space p → ℂ) (r : Fin p) (hD : Integrable D volume) (hweak : HasWeakCoordinateDerivative G D r) : ∀ᵐ x ∂volume, x ∉ tsupport G → D x = 0 := by apply (isClosed_tsupport G).isOpen_compl.ae_eq_zero_of_integral_contDiff_smul_eq_zero (hD.locallyIntegrable.locallyIntegrableOn _) intro g hg hgc hgs let ψ : Space p → ℂ := fun x => (g x : ℂ) have hψ : ContDiff ℝ ∞ ψ := Complex.ofRealCLM.contDiff.comp hg have hψc : HasCompactSupport ψ := hgc.comp_left (g := ofReal) Complex.ofReal_zero have hψs : tsupport ψ ⊆ tsupport g := tsupport_comp_subset (g := ofReal) Complex.ofReal_zero g have hz : (∫ x, G x * coordinateDerivative ψ r x) = 0 := by apply integral_eq_zero_of_ae filter_upwards [] with x by_cases hx : x ∈ tsupport G · have hn : x ∉ tsupport ψ := fun h => hgs (hψs h) hx simp [coordinateDerivative, fderiv_of_notMem_tsupport ℝ hn] · simp [image_eq_zero_of_notMem_tsupport hx] have hw := hweak ψ hψ hψc have hi : (∫ x, D x * ψ x) = 0 := neg_eq_zero.mp (hw.symm.trans hz) simpa [ψ, mul_comm, Complex.real_smul] using hi -
integrable_weak_test_productstheorem — Products with an arbitrary smooth test and its coordinate derivative are integrable for a compactly supported L1 function and its L1 weak derivative.hypothesesp :sharedℕG D :Space p → ℂr :Fin phG :hD :hGc :hweak :φ :Space p → ℂhφ :ContDiff ℝ ∞ φProof (Lean source)
theorem integrable_weak_test_products (G D : Space p → ℂ) (r : Fin p) (hG : Integrable G volume) (hD : Integrable D volume) (hGc : HasCompactSupport G) (hweak : HasWeakCoordinateDerivative G D r) (φ : Space p → ℂ) (hφ : ContDiff ℝ ∞ φ) : Integrable (fun x => G x * coordinateDerivative φ r x) volume ∧ Integrable (fun x => D x * φ x) volume := by obtain ⟨χ, hχ, hχc, hχone⟩ := exists_spatial_cutoff G hGc have hc : Continuous (coordinateDerivative φ r) := (hφ.continuous_fderiv (by simp)).clm_apply continuous_const have hGprod : Integrable (fun x => G x * (χ x * coordinateDerivative φ r x)) volume := by simpa only [smul_eq_mul, Pi.mul_apply] using hG.locallyIntegrable.integrable_smul_right_of_hasCompactSupport (hχ.continuous.mul hc) hχc.mul_right have hDprod : Integrable (fun x => D x * (χ x * φ x)) volume := by simpa only [smul_eq_mul, Pi.mul_apply] using hD.locallyIntegrable.integrable_smul_right_of_hasCompactSupport (hχ.continuous.mul hφ.continuous) hχc.mul_right constructor · apply hGprod.congr filter_upwards [] with x by_cases hx : x ∈ tsupport G · simp [(hχone x hx).eq_of_nhds] · simp [image_eq_zero_of_notMem_tsupport hx] · apply hDprod.congr filter_upwards [weakDerivative_zero_off_support G D r hD hweak] with x hxD by_cases hx : x ∈ tsupport G · simp [(hχone x hx).eq_of_nhds] · simp [hxD hx] -
weakIBP_smooth_testtheorem — Spatial integration by parts extends from compact smooth tests to every smooth test when the function has compact support and its weak derivative is integrable.hypothesesconclusion(∫ x, G x * coordinateDerivative φ r x) = -(∫ x, D x * φ x)Proof (Lean source)
theorem weakIBP_smooth_test (G D : Space p → ℂ) (r : Fin p) (hD : Integrable D volume) (hGc : HasCompactSupport G) (hweak : HasWeakCoordinateDerivative G D r) (φ : Space p → ℂ) (hφ : ContDiff ℝ ∞ φ) : (∫ x, G x * coordinateDerivative φ r x) = -(∫ x, D x * φ x) := by obtain ⟨χ, hχ, hχc, hχone⟩ := exists_spatial_cutoff G hGc have hw := hweak (fun x => χ x * φ x) (hχ.mul hφ) hχc.mul_right have hleft : (fun x => G x * coordinateDerivative (fun y => χ y * φ y) r x) =ᵐ[volume] (fun x => G x * coordinateDerivative φ r x) := by filter_upwards [] with x by_cases hx : x ∈ tsupport G · have hχx : χ x = 1 := (hχone x hx).eq_of_nhds have hχd : fderiv ℝ χ x = 0 := by simpa using (hχone x hx).fderiv_eq (𝕜 := ℝ) simp only [coordinateDerivative, fderiv_fun_mul ((hχ.differentiable (by simp)).differentiableAt) ((hφ.differentiable (by simp)).differentiableAt), hχx, hχd, add_apply, smul_apply, zero_apply, smul_zero, add_zero, one_smul] · simp [image_eq_zero_of_notMem_tsupport hx] have hright : (fun x => D x * (χ x * φ x)) =ᵐ[volume] (fun x => D x * φ x) := by filter_upwards [weakDerivative_zero_off_support G D r hD hweak] with x hxD by_cases hx : x ∈ tsupport G · simp [(hχone x hx).eq_of_nhds] · simp [hxD hx] rw [integral_congr_ae hleft, integral_congr_ae hright] at hw exact hw -
contDiff_angular_phasetheorem — The angular exponential phase is smooth as a function of spatial position.hypothesesp :sharedℕw :Space pProof (Lean source)
theorem contDiff_angular_phase (w : Space p) : ContDiff ℝ ∞ (fun u : Space p => exp (-I * ((∑ r, w r * u r : ℝ) : ℂ))) := by have h : ContDiff ℝ ∞ (fun u : Space p => (innerSL ℝ w) u) := (innerSL ℝ w).contDiff have hs : (fun u : Space p => (innerSL ℝ w) u) = (fun u => ∑ r, w r * u r) := by funext u simp [PiLp.inner_apply, RCLike.inner_apply, mul_comm] rw [hs] at h exact (contDiff_const.mul (Complex.ofRealCLM.contDiff.comp h)).cexp -
coordinateDerivative_angular_phasetheorem — Differentiating the angular exponential phase along a coordinate produces minus the imaginary unit times that frequency coordinate times the phase.hypothesesProof (Lean source)
theorem coordinateDerivative_angular_phase (w : Space p) (r : Fin p) (u : Space p) : coordinateDerivative (fun x : Space p => exp (-I * ((∑ s, w s * x s : ℝ) : ℂ))) r u = -I * (w r : ℂ) * exp (-I * ((∑ s, w s * u s : ℝ) : ℂ)) := by have hs : (innerSL ℝ w : Space p → ℝ) = (fun x => ∑ s, w s * x s) := by funext x simp [PiLp.inner_apply, RCLike.inner_apply, mul_comm] have hr := (innerSL ℝ w).hasFDerivAt (x := u) rw [hs] at hr have h := ((Complex.ofRealCLM.hasFDerivAt.comp u hr).const_mul (-I)).cexp simp only [Function.comp_def, Complex.ofRealCLM_apply] at h rw [coordinateDerivative, h.fderiv] simp [ContinuousLinearMap.comp_apply, coordinateVector, PiLp.inner_apply, RCLike.inner_apply, mul_comm] -
angularFourier_weakDerivativetheorem — The angular transform of an integrable weak coordinate derivative equals the imaginary unit times that frequency coordinate times the transform of the compactly supported spatial function, at every frequency.Proof (Lean source)
theorem angularFourier_weakDerivative (G D : Space p → ℂ) (r : Fin p) (hD : Integrable D volume) (hGc : HasCompactSupport G) (hweak : HasWeakCoordinateDerivative G D r) (w : Space p) : angularFourier D w = I * (w r : ℂ) * angularFourier G w := by have hw := weakIBP_smooth_test G D r hD hGc hweak _ (contDiff_angular_phase w) simp_rw [coordinateDerivative_angular_phase] at hw have hi : (∫ u, exp (-I * ((∑ s, w s * u s : ℝ) : ℂ)) * D u) = I * (w r : ℂ) * (∫ u, exp (-I * ((∑ s, w s * u s : ℝ) : ℂ)) * G u) := by calc _ = - (∫ u, G u * (-I * (w r : ℂ) * exp (-I * ((∑ s, w s * u s : ℝ) : ℂ)))) := by simpa only [mul_comm, neg_neg] using (congrArg neg hw).symm _ = _ := by simp_rw [show ∀ u : Space p, G u * (-I * (w r : ℂ) * exp (-I * ((∑ s, w s * u s : ℝ) : ℂ))) = (-I * (w r : ℂ)) * (exp (-I * ((∑ s, w s * u s : ℝ) : ℂ)) * G u) by intro u; ring] rw [integral_const_mul] ring unfold angularFourier rw [hi] simp only [Complex.real_smul] ring -
integrable_complexifytheorem — Complexification preserves L1 integrability of a real spatial function.hypothesesconclusionProof (Lean source)
theorem integrable_complexify (G : Space p → ℝ) (hG : Integrable G volume) : Integrable (complexify G) volume := by exact hG.ofReal -
memLp_complexifytheorem — Complexification preserves L2 membership of a real spatial function.hypothesesconclusionProof (Lean source)
theorem memLp_complexify (G : Space p → ℝ) (hG : MemLp G 2 volume) : MemLp (complexify G) 2 volume := by exact hG.ofReal -
hasCompactSupport_complexifytheorem — Complexification preserves compact support of a real spatial function.hypothesesconclusionProof (Lean source)
theorem hasCompactSupport_complexify (G : Space p → ℝ) (hG : HasCompactSupport G) : HasCompactSupport (complexify G) := by exact hG.comp_left (g := ofReal) Complex.ofReal_zero -
l2Energy_complexifytheorem — Complexification leaves squared spatial energy unchanged.Proof (Lean source)
theorem l2Energy_complexify (G : Space p → ℝ) : l2Energy (complexify G) = l2Energy G := by simp only [l2Energy, complexify, Complex.norm_real, Real.norm_eq_abs] -
integrable_compact_test_productstheorem — An integrable spatial function and an integrable proposed derivative have integrable products with a compact smooth test and its coordinate derivative.hypothesesProof (Lean source)
theorem integrable_compact_test_products (G D : Space p → ℂ) (r : Fin p) (hG : Integrable G volume) (hD : Integrable D volume) (φ : Space p → ℂ) (hφ : ContDiff ℝ ∞ φ) (hφc : HasCompactSupport φ) : Integrable (fun x => G x * coordinateDerivative φ r x) volume ∧ Integrable (fun x => D x * φ x) volume := by have hc : Continuous (coordinateDerivative φ r) := (hφ.continuous_fderiv (by simp)).clm_apply continuous_const constructor · simpa only [smul_eq_mul] using hG.locallyIntegrable.integrable_smul_right_of_hasCompactSupport hc (hφc.fderiv_apply (𝕜 := ℝ) (coordinateVector r)) · simpa only [smul_eq_mul] using hD.locallyIntegrable.integrable_smul_right_of_hasCompactSupport hφ.continuous hφc -
hasDerivAt_test_coordinate_slicetheorem — Restricting a smooth complex scalar test to a canonical coordinate line gives a differentiable one-dimensional test with the specified coordinate derivative.hypothesesconclusionHasDerivAt (fun s => φ (updateCoordinate x r s)) (coordinateDerivative φ r (updateCoordinate x r t)) tProof (Lean source)
theorem hasDerivAt_test_coordinate_slice (φ : Space p → ℂ) (hφ : ContDiff ℝ ∞ φ) (x : Space p) (r : Fin p) (t : ℝ) : HasDerivAt (fun s => φ (updateCoordinate x r s)) (coordinateDerivative φ r (updateCoordinate x r t)) t := by let L : (Fin p → ℝ) →L[ℝ] Space p := (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin p => ℝ)).symm.toContinuousLinearMap have hu := (L.hasFDerivAt.comp t (hasFDerivAt_update (fun s => x s) (i := r) t)).hasDerivAt have he : (L ∘L ContinuousLinearMap.pi (single r (id ℝ ℝ))) 1 = coordinateVector r := by apply PiLp.ext intro s by_cases hs : s = r <;> simp [L, coordinateVector, Pi.single_apply, hs] rw [he] at hu exact (hφ.differentiable (by simp)).differentiableAt.hasFDerivAt.comp_hasDerivAt t hu -
continuous_test_coordinate_slice_derivativetheorem — The coordinate derivative of a smooth test remains continuous when restricted to a coordinate line.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem continuous_test_coordinate_slice_derivative (φ : Space p → ℂ) (hφ : ContDiff ℝ ∞ φ) (x : Space p) (r : Fin p) : Continuous (fun t => coordinateDerivative φ r (updateCoordinate x r t)) := by have hc : Continuous (coordinateDerivative φ r) := (hφ.continuous_fderiv (by simp)).clm_apply continuous_const apply hc.comp unfold updateCoordinate apply (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin p => ℝ)).symm.continuous.comp exact (continuous_update (A := fun _ : Fin p => ℝ) r).comp ((continuous_const (y := fun s => x s)).prodMk continuous_id) -
integrable_coordinate_slices_aetheorem — A globally integrable Euclidean scalar function is integrable on almost every coordinate slice with respect to the exact remaining-coordinate volume.hypothesesconclusionProof (Lean source)
theorem integrable_coordinate_slices_ae (F : Space p → ℂ) (hF : Integrable F volume) (r : Fin p) : ∀ᵐ z : RemainingCoordinates r ∂volume, Integrable (fun t : ℝ => F (insertCoordinate r z t)) volume := by have hm : Measurable (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) := by unfold insertCoordinate apply (WithLp.measurable_toLp 2 (Fin p → ℝ)).comp apply measurable_pi_lambda intro s split_ifs <;> fun_prop have hp : MeasurePreserving (fun zt : RemainingCoordinates r × ℝ => insertCoordinate r zt.1 zt.2) (volume.prod volume) volume := ⟨hm, map_insertCoordinate_volume r⟩ exact (hp.integrable_comp_of_integrable hF).prod_right_ae -
realSliceIBP_complex_testtheorem — Real coordinate-slice integration by parts also holds for complex C1 test pairs whenever the two complex slice products are integrable.hypothesesp :sharedℕG :Space p → ℝhslice :HasRealSliceIBP G Dr :Fin px :Space pv v' :ℝ → ℂhv :∀ t, HasDerivAt v (v' t) thv' :Continuous v'hGv' :hDv :conclusion(∫ t : ℝ, (G (updateCoordinate x r t) : ℂ) * v' t)= -(∫ t : ℝ, (D r (updateCoordinate x r t) : ℂ) * v t)Proof (Lean source)
theorem realSliceIBP_complex_test (G : Space p → ℝ) (D : Fin p → Space p → ℝ) (hslice : HasRealSliceIBP G D) (r : Fin p) (x : Space p) (v v' : ℝ → ℂ) (hv : ∀ t, HasDerivAt v (v' t) t) (hv' : Continuous v') (hGv' : Integrable (fun t => (G (updateCoordinate x r t) : ℂ) * v' t) volume) (hDv : Integrable (fun t => (D r (updateCoordinate x r t) : ℂ) * v t) volume) : (∫ t : ℝ, (G (updateCoordinate x r t) : ℂ) * v' t) = -(∫ t : ℝ, (D r (updateCoordinate x r t) : ℂ) * v t) := by have hre := hslice r x (fun t => (v t).re) (fun t => (v' t).re) (fun t => Complex.reCLM.hasFDerivAt.comp_hasDerivAt t (hv t)) (Complex.reCLM.continuous.comp hv') have him := hslice r x (fun t => (v t).im) (fun t => (v' t).im) (fun t => Complex.imCLM.hasFDerivAt.comp_hasDerivAt t (hv t)) (Complex.imCLM.continuous.comp hv') apply Complex.ext · change RCLike.re (∫ t : ℝ, (G (updateCoordinate x r t) : ℂ) * v' t) = -RCLike.re (∫ t : ℝ, (D r (updateCoordinate x r t) : ℂ) * v t) rw [← integral_re hGv', ← integral_re hDv] simpa only [RCLike.re_eq_complex_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] using hre · change RCLike.im (∫ t : ℝ, (G (updateCoordinate x r t) : ℂ) * v' t) = -RCLike.im (∫ t : ℝ, (D r (updateCoordinate x r t) : ℂ) * v t) rw [← integral_im hGv', ← integral_im hDv] simpa only [RCLike.im_eq_complex_im, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, zero_mul, add_zero] using him -
realSliceIBP_coordinates_ifftheorem — The Euclidean slice interface is exactly the ordinary coordinate-update interface on the finite product, with no change of constants or measure.hypothesesconclusionHasRealSliceIBP (fun x : Space p => G (fun s => x s)) (fun r x => D r (fun s => x s))↔ (∀ (r : Fin p) (x : Fin p → ℝ) (v v' : ℝ → ℝ), (∀ t, HasDerivAt v (v' t) t) → Continuous v' → (∫ t : ℝ, G (update x r t) * v' t) = -(∫ t : ℝ, D r (update x r t) * v t))Proof (Lean source)
theorem realSliceIBP_coordinates_iff (G : (Fin p → ℝ) → ℝ) (D : Fin p → (Fin p → ℝ) → ℝ) : HasRealSliceIBP (fun x : Space p => G (fun s => x s)) (fun r x => D r (fun s => x s)) ↔ (∀ (r : Fin p) (x : Fin p → ℝ) (v v' : ℝ → ℝ), (∀ t, HasDerivAt v (v' t) t) → Continuous v' → (∫ t : ℝ, G (update x r t) * v' t) = -(∫ t : ℝ, D r (update x r t) * v t)) := by constructor · intro h r x v v' hv hv' simpa only [updateCoordinate, PiLp.toLp_apply] using h r (toLp 2 x) v v' hv hv' · intro h r x v v' hv hv' simpa only [updateCoordinate, PiLp.toLp_apply] using h r (fun s => x s) v v' hv hv'
Estimate 1 core · 1 supporting The main theorem gives the geometric interpolation bound directly in terms of the frequency-space squared L² norms of G and G', with the normalization constant visible. ★ inverse_weightedEnergy_le
Quantitative weighted inverse-Fourier estimates
The main theorem gives the geometric interpolation bound directly in terms of the frequency-space squared L² norms of G and G', with the normalization constant visible. The scale-dependent variant is useful for bandwidth families. Compactness and C¹ regularity, together with standard absolute-integrability inversion hypotheses, suffice.
theorem inverse_weightedEnergy_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
For a complex frequency multiplier G with admissible compact inverse-Fourier data and a moment exponent κ between zero and two, the function |v|^κ·|g(v)|², with g the inverse Fourier transform of G, is integrable, and its integral is at most E₀^(1 − κ/2)·((2π)⁻²·E₁)^(κ/2), where E₀ is the integral of |G|² and E₁ the integral of |G′|².
Formal statement
hypotheses
conclusion
conclusion 1
Integrable (fun v => |v| ^ κ * ‖𝓕⁻ G v‖ ^ 2)
conclusion 2
weightedEnergy κ (𝓕⁻ G)
Proof (Lean source)
theorem inverse_weightedEnergy_le (G : ℝ → ℂ) (hG : CompactInverseData G)
(κ : ℝ) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) :
Integrable (fun v => |v| ^ κ * ‖𝓕⁻ G v‖ ^ 2) ∧
weightedEnergy κ (𝓕⁻ G) ≤
(energy G) ^ (1 - κ / 2) *
((2 * pi)⁻¹ ^ 2 * energy (deriv G)) ^ (κ / 2) := by
obtain ⟨h0, h2, e0, e2⟩ := inverse_energy_endpoints G hG
refine ⟨integrable_weightedEnergy (𝓕⁻ G) κ
hG.integrable_inverse.aestronglyMeasurable hκ0 hκ2 h0 h2, ?_⟩
simpa only [e0, e2] using weightedEnergy_le_interpolation (𝓕⁻ G) κ
hκ0 hκ2 h0 h2
1 supporting declaration (lemmas, instances)
-
inverse_weightedEnergy_le_scaledtheorem — A complex frequency multiplier with admissible compact inverse-Fourier data, a moment exponent in the interval from zero to two, and a positive reference scale satisfy the scale-dependent additive inverse-Fourier weighted-energy bound.hypothesesconclusionweightedEnergy κ (𝓕⁻ G)Proof (Lean source)
theorem inverse_weightedEnergy_le_scaled (G : ℝ → ℂ) (hG : CompactInverseData G) (κ h : ℝ) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) (hh : 0 < h) : weightedEnergy κ (𝓕⁻ G) ≤ h ^ κ * energy G + h ^ (κ - 2) * (2 * pi)⁻¹ ^ 2 * energy (deriv G) := by obtain ⟨h0, h2, e0, e2⟩ := inverse_energy_endpoints G hG simpa only [e0, e2, mul_assoc] using weightedEnergy_le_scaled (𝓕⁻ G) κ h hG.integrable_inverse.aestronglyMeasurable hκ0 hκ2 hh h0 h2
Interpolation 1 core · 3 supporting The geometric interpolation inequality assumes only integrable zeroth and second moments; the integrability statement and the additive bound also assume an almost-everywhere strongly measurable function. ★ weightedEnergy_le_interpolation
Interpolating absolute weighted L² energies
The geometric interpolation inequality assumes only integrable zeroth and second moments; the integrability statement and the additive bound also assume an almost-everywhere strongly measurable function. Both the geometric interpolation inequality and a scale-dependent additive bound include κ = 0 and κ = 2. Integrability of the weighted integrand is proved separately, so the real integral's nonintegrable-zero convention does not make the estimates meaningless.
theorem weightedEnergy_le_interpolation reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
For a complex-valued function g on the real line, a moment exponent κ between zero and two, and integrable |g|² and v²·|g(v)|², the integral of |v|^κ·|g(v)|² is at most E₀^(1 − κ/2)·E₂^(κ/2), where E₀ is the integral of |g|² and E₂ the integral of v²·|g(v)|².
Formal statement
hypotheses
g :
ℝ → ℂ
κ :
ℝ
hκ0 :
0 ≤ κ
hκ2 :
κ ≤ 2
h0 :
Integrable (fun v => ‖g v‖ ^ 2)
h2 :
Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)
conclusion
Proof (Lean source)
theorem weightedEnergy_le_interpolation (g : ℝ → ℂ) (κ : ℝ)
(hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2)
(h0 : Integrable (fun v => ‖g v‖ ^ 2))
(h2 : Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)) :
weightedEnergy κ g ≤
(energy g) ^ (1 - κ / 2) * (weightedEnergy 2 g) ^ (κ / 2) := by
rcases eq_or_lt_of_le hκ0 with hk | hk
· subst κ
simp [weightedEnergy_zero]
rcases eq_or_lt_of_le hκ2 with hk2 | hk2
· subst κ
simp
let a : ℝ := 1 - κ / 2
let b : ℝ := κ / 2
have ha : 0 < a := by dsimp [a]; linarith
have hb : 0 < b := by dsimp [b]; linarith
have hab : a + b = 1 := by dsimp [a, b]; ring
have hpq : a⁻¹.HolderConjugate b⁻¹ := Real.HolderConjugate.inv_inv ha hb hab
have hmem : ∀ (f : ℝ → ℝ) (c : ℝ), (∀ v, 0 ≤ f v) →
Integrable f → 0 < c →
MemLp (fun v => f v ^ c) (ofReal c⁻¹) := by
intro f c hf hi hc
have hm := (Real.continuous_rpow_const hc.le).comp_aestronglyMeasurable hi.1
apply (integrable_norm_rpow_iff hm
(ne_of_gt (ENNReal.ofReal_pos.mpr (inv_pos.mpr hc)))
ENNReal.ofReal_ne_top).mp
have hid : (fun v => ‖f v ^ c‖ ^ (ofReal c⁻¹).toReal) = f := by
funext v
rw [ENNReal.toReal_ofReal (inv_pos.mpr hc).le, Real.norm_eq_abs,
abs_of_nonneg (Real.rpow_nonneg (hf v) c),
← Real.rpow_mul (hf v), mul_inv_cancel₀ hc.ne', Real.rpow_one]
rwa [hid]
have hf := hmem (fun v => ‖g v‖ ^ 2) a (fun v => sq_nonneg _) h0 ha
have hh := hmem (fun v => v ^ 2 * ‖g v‖ ^ 2) b
(fun v => mul_nonneg (sq_nonneg v) (sq_nonneg _)) h2 hb
have hpow0 : (fun v => ((‖g v‖ ^ 2 : ℝ) ^ a) ^ a⁻¹) = (fun v => ‖g v‖ ^ 2) := by
funext v
rw [← Real.rpow_mul (sq_nonneg _), mul_inv_cancel₀ ha.ne', Real.rpow_one]
have hpow2 : (fun v => ((v ^ 2 * ‖g v‖ ^ 2 : ℝ) ^ b) ^ b⁻¹) =
(fun v => v ^ 2 * ‖g v‖ ^ 2) := by
funext v
rw [← Real.rpow_mul (mul_nonneg (sq_nonneg _) (sq_nonneg _)),
mul_inv_cancel₀ hb.ne', Real.rpow_one]
have hprod : (fun v => (‖g v‖ ^ 2 : ℝ) ^ a *
(v ^ 2 * ‖g v‖ ^ 2) ^ b) = (fun v => |v| ^ κ * ‖g v‖ ^ 2) := by
funext v
rw [Real.mul_rpow (sq_nonneg v) (sq_nonneg _)]
calc
(‖g v‖ ^ 2 : ℝ) ^ a * ((v ^ 2 : ℝ) ^ b * (‖g v‖ ^ 2 : ℝ) ^ b) =
(v ^ 2 : ℝ) ^ b * ((‖g v‖ ^ 2 : ℝ) ^ a * (‖g v‖ ^ 2 : ℝ) ^ b) := by ring
_ = (v ^ 2 : ℝ) ^ b * ‖g v‖ ^ 2 := by
rw [← Real.rpow_add_of_nonneg (sq_nonneg _) ha.le hb.le, hab, Real.rpow_one]
_ = |v| ^ κ * ‖g v‖ ^ 2 := by
rw [← sq_abs, ← Real.rpow_two, ← Real.rpow_mul (abs_nonneg v)]
congr 2
dsimp [b]
ring
have hhölder := integral_mul_le_Lp_mul_Lq_of_nonneg hpq
(Filter.Eventually.of_forall fun v => Real.rpow_nonneg (sq_nonneg ‖g v‖) a)
(Filter.Eventually.of_forall fun v =>
Real.rpow_nonneg (mul_nonneg (sq_nonneg v) (sq_nonneg ‖g v‖)) b) hf hh
simp only [one_div, inv_inv] at hhölder
rw [hpow0, hpow2, hprod] at hhölder
rw [weightedEnergy_two]
simpa only [weightedEnergy, energy, a, b] using hhölder
3 supporting declarations (lemmas, instances)
-
abs_rpow_le_scaled_quadratictheorem — A moment exponent in the interval from zero to two, a positive reference scale, and a real location give the stated bound of its absolute power by zeroth and quadratic weights.hypothesesκ h v :ℝhκ0 :0 ≤ κhκ2 :κ ≤ 2hh :0 < hconclusion|v| ^ κ ≤ h ^ κ + h ^ (κ - 2) * v ^ 2Proof (Lean source)
theorem abs_rpow_le_scaled_quadratic (κ h v : ℝ) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) (hh : 0 < h) : |v| ^ κ ≤ h ^ κ + h ^ (κ - 2) * v ^ 2 := by by_cases hv : |v| ≤ h · exact (Real.rpow_le_rpow (abs_nonneg v) hv hκ0).trans (le_add_of_nonneg_right (mul_nonneg (Real.rpow_nonneg hh.le _) (sq_nonneg v))) · have hvpos : 0 < |v| := lt_trans hh (lt_of_not_ge hv) have hpow : |v| ^ (κ - 2) ≤ h ^ (κ - 2) := Real.rpow_le_rpow_of_nonpos hh (le_of_lt (lt_of_not_ge hv)) (by linarith) have hid : |v| ^ κ = |v| ^ (κ - 2) * v ^ 2 := by rw [← sq_abs, ← Real.rpow_two, ← Real.rpow_add hvpos] congr 1 ring rw [hid] exact (mul_le_mul_of_nonneg_right hpow (sq_nonneg v)).trans (le_add_of_nonneg_left (Real.rpow_nonneg hh.le _)) -
integrable_weightedEnergytheorem — A complex-valued function with almost-everywhere strong measurability, a moment exponent in the interval from zero to two, and finite ordinary and quadratic squared energies have an integrable weighted squared energy.hypothesesg :ℝ → ℂκ :ℝhg :hκ0 :0 ≤ κhκ2 :κ ≤ 2h0 :Integrable (fun v => ‖g v‖ ^ 2)h2 :Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)conclusionIntegrable (fun v => |v| ^ κ * ‖g v‖ ^ 2)Proof (Lean source)
theorem integrable_weightedEnergy (g : ℝ → ℂ) (κ : ℝ) (hg : AEStronglyMeasurable g) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) (h0 : Integrable (fun v => ‖g v‖ ^ 2)) (h2 : Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)) : Integrable (fun v => |v| ^ κ * ‖g v‖ ^ 2) := by have hm : AEStronglyMeasurable (fun v : ℝ => |v| ^ κ * ‖g v‖ ^ 2) := by exact ((Real.continuous_rpow_const hκ0).comp continuous_abs).aestronglyMeasurable.mul (hg.norm.pow 2) refine (h0.add h2).mono' hm (Filter.Eventually.of_forall fun v => ?_) rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (Real.rpow_nonneg (abs_nonneg v) κ) (sq_nonneg _))] have hb := abs_rpow_le_scaled_quadratic κ 1 v hκ0 hκ2 zero_lt_one simp only [Real.one_rpow, one_mul] at hb simpa only [Pi.add_apply, add_mul, one_mul] using mul_le_mul_of_nonneg_right hb (sq_nonneg ‖g v‖) -
weightedEnergy_le_scaledtheorem — A complex-valued function with almost-everywhere strong measurability, a moment exponent in the interval from zero to two, a positive reference scale, and finite ordinary and quadratic squared energies satisfy the scale-dependent additive weighted-energy bound.hypothesesg :ℝ → ℂκ h :ℝhg :hκ0 :0 ≤ κhκ2 :κ ≤ 2hh :0 < hh0 :Integrable (fun v => ‖g v‖ ^ 2)h2 :Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)conclusionProof (Lean source)
theorem weightedEnergy_le_scaled (g : ℝ → ℂ) (κ h : ℝ) (hg : AEStronglyMeasurable g) (hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) (hh : 0 < h) (h0 : Integrable (fun v => ‖g v‖ ^ 2)) (h2 : Integrable (fun v => v ^ 2 * ‖g v‖ ^ 2)) : weightedEnergy κ g ≤ h ^ κ * energy g + h ^ (κ - 2) * weightedEnergy 2 g := by have hw := integrable_weightedEnergy g κ hg hκ0 hκ2 h0 h2 have hr := (h0.const_mul (h ^ κ)).add (h2.const_mul (h ^ (κ - 2))) have hi := integral_mono hw hr (fun v => by simpa only [Pi.add_apply, add_mul, mul_assoc] using mul_le_mul_of_nonneg_right (abs_rpow_le_scaled_quadratic κ h v hκ0 hκ2 hh) (sq_nonneg ‖g v‖)) rw [weightedEnergy_two] simpa only [weightedEnergy, energy, Pi.add_apply, add_mul, mul_assoc, integral_add (h0.const_mul _) (h2.const_mul _), integral_const_mul] using hi
WeightedSpecialization 1 core · 1 supporting This theorem combines the frequency norm bounds with the reusable scaled Fourier estimate, keeping every profile constant visible. ★ inverseGaussian_weightedEnergy_le
Weighted inverse Gaussian multiplier specialization
This theorem combines the frequency norm bounds with the reusable scaled Fourier estimate, keeping every profile constant visible. It is independent of subsequent physical-space averaging, so the frequency specialization can be checked on its own. The multiplier profile and all inversion hypotheses are supplied by the caller; the weighted physical-space bound is derived here.
theorem inverseGaussian_weightedEnergy_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Fourier
For a compactly supported continuously differentiable frequency profile F, a moment exponent κ between zero and two, a nonnegative Gaussian scale σ and positive bandwidth h, and nonnegative envelope constants a and b, suppose F vanishes outside the interval of radius 3/(πh) around zero, |F| ≤ a·h and |F′| ≤ b·h² everywhere, and the inverse Fourier transforms of the inverse-Gaussian multiplier of F and of its derivative are integrable. Then, writing g for the inverse Fourier transform of that multiplier, |v|^κ·|g(v)|² is integrable and its integral is at most (6/π)·(a² + (2π)⁻²·(b + 12π·a)²)·h^(κ+1)·(1 + σ/h)⁴·exp(36·(σ/h)²).
Formal statement
hypotheses
F :
ℝ → ℂ
κ σ h a b :
ℝ
hF :
ContDiff ℝ 1 F
hcompact :
hκ0 :
0 ≤ κ
hκ2 :
κ ≤ 2
hh :
0 < h
hσ :
0 ≤ σ
ha :
0 ≤ a
hb :
0 ≤ b
hbound :
∀ ξ, ‖F ξ‖ ≤ a * h
hderiv :
∀ ξ, ‖deriv F ξ‖ ≤ b * h ^ 2
hinv :
Integrable (𝓕⁻ (inverseGaussian σ F))
hinvD :
conclusion
conclusion 1
Integrable (fun v => |v| ^ κ * ‖𝓕⁻ (inverseGaussian σ F) v‖ ^ 2)
conclusion 2
weightedEnergy κ (𝓕⁻ (inverseGaussian σ F))
Proof (Lean source)
theorem inverseGaussian_weightedEnergy_le (F : ℝ → ℂ) (κ σ h a b : ℝ)
(hF : ContDiff ℝ 1 F) (hcompact : HasCompactSupport F)
(hκ0 : 0 ≤ κ) (hκ2 : κ ≤ 2) (hh : 0 < h) (hσ : 0 ≤ σ)
(ha : 0 ≤ a) (hb : 0 ≤ b)
(hsupport : support F ⊆ Icc (-(3 / (pi * h))) (3 / (pi * h)))
(hbound : ∀ ξ, ‖F ξ‖ ≤ a * h) (hderiv : ∀ ξ, ‖deriv F ξ‖ ≤ b * h ^ 2)
(hinv : Integrable (𝓕⁻ (inverseGaussian σ F)))
(hinvD : Integrable (𝓕⁻ (deriv (inverseGaussian σ F)))) :
Integrable (fun v => |v| ^ κ * ‖𝓕⁻ (inverseGaussian σ F) v‖ ^ 2) ∧
weightedEnergy κ (𝓕⁻ (inverseGaussian σ F)) ≤
((6 / pi) * (a ^ 2 + (2 * pi)⁻¹ ^ 2 *
(b + 12 * pi * a) ^ 2)) *
h ^ (κ + 1) * (1 + σ / h) ^ 4 * exp (36 * (σ / h) ^ 2) := by
have hG := inverseGaussian_compactInverseData F σ hF hcompact hinv hinvD
refine ⟨(inverse_weightedEnergy_le (inverseGaussian σ F) hG κ hκ0 hκ2).1, ?_⟩
have he := inverseGaussian_energy_le F σ h a hF.continuous hh ha hsupport hbound
have heD := inverseGaussian_deriv_energy_le F σ h a b hF hh hσ ha hb
hsupport hbound hderiv
have hpoly : 1 ≤ (1 + σ / h) ^ 4 :=
one_le_pow₀ (by linarith [div_nonneg hσ hh.le])
have hpow1 : h ^ κ * h = h ^ (κ + 1) := by
rw [Real.rpow_add hh, Real.rpow_one]
have hpow3 : h ^ (κ - 2) * h ^ 3 = h ^ (κ + 1) := by
rw [← Real.rpow_natCast h 3, ← Real.rpow_add hh]
congr 1
norm_num
ring
have hepoly : (6 / pi) * a ^ 2 * h * exp (36 * (σ / h) ^ 2) ≤
(6 / pi) * a ^ 2 * h * (1 + σ / h) ^ 4 *
exp (36 * (σ / h) ^ 2) := by
have hp := mul_le_mul_of_nonneg_left hpoly
(show 0 ≤ (6 / pi) * a ^ 2 * h by positivity)
exact mul_le_mul_of_nonneg_right (by simpa only [mul_one] using hp)
(Real.exp_pos _).le
calc
_ ≤ h ^ κ * energy (inverseGaussian σ F) +
h ^ (κ - 2) * (2 * pi)⁻¹ ^ 2 * energy (deriv (inverseGaussian σ F)) :=
inverse_weightedEnergy_le_scaled (inverseGaussian σ F) hG κ h hκ0 hκ2 hh
_ ≤ h ^ κ * ((6 / pi) * a ^ 2 * h * (1 + σ / h) ^ 4 *
exp (36 * (σ / h) ^ 2)) +
h ^ (κ - 2) * (2 * pi)⁻¹ ^ 2 *
((6 / pi) * (b + 12 * pi * a) ^ 2 * h ^ 3 *
(1 + σ / h) ^ 4 * exp (36 * (σ / h) ^ 2)) :=
add_le_add (mul_le_mul_of_nonneg_left (he.trans hepoly) (by positivity))
(mul_le_mul_of_nonneg_left heD (by positivity))
_ = (6 / pi) * a ^ 2 * (h ^ κ * h) * (1 + σ / h) ^ 4 *
exp (36 * (σ / h) ^ 2) +
(6 / pi) * (2 * pi)⁻¹ ^ 2 * (b + 12 * pi * a) ^ 2 *
(h ^ (κ - 2) * h ^ 3) * (1 + σ / h) ^ 4 *
exp (36 * (σ / h) ^ 2) := by ring
_ = _ := by rw [hpow1, hpow3]; ring
1 supporting declaration (lemmas, instances)
-
inverseGaussian_compactInverseDatatheorem — A complex frequency profile with one continuous derivative and compact spectral support, a Gaussian scale parameter, and integrable inverse transforms of the multiplier and its derivative give admissible compact inverse-Fourier data for the inverse-Gaussian multiplier.hypothesesconclusionProof (Lean source)
theorem inverseGaussian_compactInverseData (F : ℝ → ℂ) (σ : ℝ) (hF : ContDiff ℝ 1 F) (hcompact : HasCompactSupport F) (hinv : Integrable (𝓕⁻ (inverseGaussian σ F))) (hinvD : Integrable (𝓕⁻ (deriv (inverseGaussian σ F)))) : CompactInverseData (inverseGaussian σ F) := by exact ⟨inverseGaussian_contDiff F σ hF, inverseGaussian_hasCompactSupport F σ hcompact, hinv, hinvD⟩