noncomputable def FourierProjection.subspaceProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] (V : Submodule ℝ E) (μ_perp : MeasureTheory.Measure ↥Vᗮ) (f : E → ℂ) (y : ↥V) : ℂ

Projection of f : E → ℂ onto a subspace V ⊂ E, defined by integrating out the orthogonal directions: (π_V f)(y) = ∫_{V^⊥} f(y + z) dμ_perp(z).

theorem FourierProjection.innerₗ_add_orthogonal_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (V : Submodule ℝ E) (y ξ : ↥V) (z : ↥Vᗮ) : ((innerₗ E) (↑y + ↑z)) ↑ξ = ((innerₗ ↥V) y) ξ

For ξ ∈ V and z ∈ V^⊥, the orthogonal component drops out of the inner product: ⟨y + z, ξ⟩_E = ⟨y, ξ⟩_V. This identifies the phase appearing in the Fourier integral on E with the phase on V.

theorem FourierProjection.fourier_projection_dictionary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] (V : Submodule ℝ E) (μ_V : MeasureTheory.Measure ↥V) (μ_perp : MeasureTheory.Measure ↥Vᗮ) (μ_E : MeasureTheory.Measure E) (f : E → ℂ) (ξ : ↥V) (hμ : ∀ (g : E → ℂ), MeasureTheory.Integrable g μ_E → ∫ (x : E), g x ∂μ_E = ∫ (y : ↥V), ∫ (z : ↥Vᗮ), g (↑y + ↑z) ∂μ_perp ∂μ_V) (hfξ_int : MeasureTheory.Integrable (fun (x : E) => Real.fourierChar (-((innerₗ E) x) ↑ξ) • f x) μ_E) : VectorFourier.fourierIntegral Real.fourierChar μ_V (innerₗ ↥V) (subspaceProjection V μ_perp f) ξ = VectorFourier.fourierIntegral Real.fourierChar μ_E (innerₗ E) f ↑ξ

Fourier projection dictionary lemma. For any subspace V ⊂ E and any frequency ξ ∈ V, $$\widehat{\pi_V f}(\xi) = \hat f(\xi),$$ i.e. the Fourier transform of the projection π_V f at ξ ∈ V equals the Fourier transform of f at the same ξ viewed in E. The proof unfolds both Fourier integrals, uses Fubini on the splitting E = V ⊕ V^⊥, and observes that the phase e(-⟨x, ξ⟩) depends only on the V-component of x (since ξ ∈ V).