Documentation

Atlas.ProjectionTheory.code.ProjectionSmoothing

noncomputable def ProjectionSmoothing.projectionAlongDirection {d : } (θ : (Metric.sphere 0 1)) (f : EuclideanSpace (Fin d)) :

The projection π_θ f : ℝ → ℂ of an function f : ℝ^d → ℂ along the direction θ ∈ S^{d−1}: at the point t ∈ ℝ it returns the integral of f over the affine hyperplane t·θ + θ^⊥, with respect to the Haar measure on θ^⊥.

Instances For
    noncomputable def ProjectionSmoothing.ckNorm (k : ) (g : ) :

    The C^k norm of a function g : ℝ → ℂ: the supremum over 0 ≤ j ≤ k and t ∈ ℝ of ‖g^(j)(t)‖.

    Instances For
      noncomputable def ProjectionSmoothing.sobolevNormSq (s : ) (g : ) :

      The inhomogeneous Sobolev H^s squared norm ∫ (1 + |ξ|²)^s |ĝ(ξ)|² dξ of a function g : ℝ → ℂ.

      Instances For
        theorem ProjectionSmoothing.sobolev_embedding (k : ) (s : ) (hs : s > 1 / 2 + k) :
        C > 0, ∀ (g : ), ckNorm k g ^ 2 C * sobolevNormSq s g

        Sobolev embedding (one dimension). If s > 1/2 + k, then the Sobolev H^s norm controls the C^k norm: there is a constant C > 0 such that ‖g‖_{C^k}² ≤ C · ‖g‖_{H^s}² for every g : ℝ → ℂ.

        noncomputable def ProjectionSmoothing.homoSobolevNormSq (s : ) (g : ) :

        The homogeneous Sobolev Ḣ^s squared norm ∫ |ξ|^{2s} |ĝ(ξ)|² dξ.

        Instances For

          Plancherel's identity on ℝ^d. For f ∈ L²(ℝ^d), ∫ |f|² = ∫ |𝓕 f|².

          Polar coordinate decomposition of ‖𝓕 f‖_{L²}². There exists C_d > 0 (the polar Jacobian constant) such that ∫ |𝓕 f|² dξ = C_d ∫_{S^{d−1}} ∫_ℝ |r|^{d−1} |𝓕 f(r θ)|² dr dσ(θ).

          Fubini step used in the Fourier slice theorem: rewriting the Fourier integral of f against the character at r θ as a one-dimensional Fourier integral of the θ-slice integral of f.

          Fourier slice theorem. For f ∈ L²(ℝ^d) and θ ∈ S^{d−1}, the 1-D Fourier transform of the projection π_θ f at r equals the d-dimensional Fourier transform of f evaluated at r·θ: 𝓕(π_θ f)(r) = 𝓕f(r θ).

          Combining polar coordinates with the Fourier slice theorem: the norm of 𝓕 f equals (up to a dimensional constant) the average over θ ∈ S^{d−1} of the homogeneous Sobolev Ḣ^{(d−1)/2} squared norm of the projection π_θ f.

          Bounded version: combining Plancherel on ℝ^d with the polar/Fourier slice identity, the spherical average of the homogeneous Sobolev Ḣ^{(d−1)/2} norms of the projections is bounded by a constant times ‖f‖_{L²}².

          1-D Plancherel for the projection: ‖𝓕(π_θ f)‖_{L²(ℝ)}² = ‖π_θ f‖_{L²(ℝ)}².

          Fubini for the projection-norm integrand: the slice integral of ‖f‖ is integrable in t and its integral over equals ‖f‖_{L¹(ℝ^d)}.

          -bound on the projection: ‖π_θ f‖_{L¹(ℝ)} ≤ ‖f‖_{L¹(ℝ^d)}.

          theorem ProjectionSmoothing.slice_integral_le_full_integral {d : } (f : EuclideanSpace (Fin d)) (hf_nn : ∀ (x : EuclideanSpace (Fin d)), 0 f x) (θ : (Metric.sphere 0 1)) (t : ) :
          (z : ↥( θ)), f (t θ + z) MeasureTheory.Measure.addHaar (x : EuclideanSpace (Fin d)), f x

          For a nonnegative function f, any slice integral ∫_{θ^⊥} f(tθ + z) dz is bounded above by the full integral ∫_{ℝ^d} f.

          Pointwise L^∞-bound on the projection by the norm of f: |π_θ f(t)| ≤ ‖f‖_{L¹(ℝ^d)} for every t.

          The norm t ↦ ‖π_θ f(t)‖ of the projection is integrable on .

          Fourier bound: ‖𝓕(π_θ f)‖_{L²(ℝ)}² ≤ ‖f‖_{L¹(ℝ^d)}². Combines the 1-D Plancherel identity with the pointwise L^∞ bound.

          Low-frequency bound: the spherical average of ∫ |𝓕(π_θ f)|² is bounded by a constant times ‖f‖_{L¹(ℝ^d)}².

          The Sobolev squared norm is nonnegative.

          The map θ ↦ ∫ |𝓕(π_θ f)|² is integrable on S^{d−1}.

          The map θ ↦ ‖π_θ f‖_{Ḣ^{(d−1)/2}}² is AEStronglyMeasurable on S^{d−1}.

          The map θ ↦ ‖π_θ f‖_{Ḣ^{(d−1)/2}}² has finite integral on S^{d−1}.

          The map θ ↦ ‖π_θ f‖_{Ḣ^{(d−1)/2}}² is integrable on S^{d−1}.

          Auxiliary integrability statement used in sobolev_norm_split: integrability of the (1+|ξ|²)^s · |ĝ|² integrand transfers to the majorant 2^{|s|}(|ĝ|² + |ξ|^{2s}|ĝ|²).

          Splitting the integral of |ĝ|² + |ξ|^{2s}|ĝ|² as the sum of two integrals, given integrability of the joint integrand.

          Pointwise control of the inhomogeneous Sobolev norm by the and homogeneous Sobolev parts: ‖g‖_{H^s}² ≤ 2^{|s|}(‖ĝ‖_{L²}² + ‖g‖_{Ḣ^s}²).

          The map θ ↦ ‖π_θ f‖_{H^{(d−1)/2}}² is AEStronglyMeasurable on S^{d−1}.

          The map θ ↦ ‖π_θ f‖_{H^{(d−1)/2}}² is integrable on S^{d−1}.

          Spherical-averaged version of sobolev_norm_split: the average inhomogeneous Sobolev norm of the projections is controlled by the sum of the averaged -Fourier norm and the averaged homogeneous Sobolev norm.

          Combined bound: the spherical average of ‖π_θ f‖_{H^{(d−1)/2}}² is integrable and bounded by a constant times ‖f‖_{L²}² + ‖f‖_{L¹}².

          Cauchy–Schwarz for a function supported in the unit closed ball: ‖f‖_{L¹}² ≤ vol(B_1) · ‖f‖_{L²}².

          For f ∈ L²(ℝ^d) supported in the unit ball, the spherical average of ‖π_θ f‖_{H^{(d−1)/2}}² is controlled by a constant times ‖f‖_{L²}².

          theorem ProjectionSmoothing.smoothing_by_projection {d : } (k : ) (hdim : (d - 1) / 2 > 1 / 2 + k) (f : EuclideanSpace (Fin d)) (hf_l2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_supp : Function.support f Metric.closedBall 0 1) :

          Theorem 6.1 (Projection smoothing). If f ∈ L²(ℝ^d) is supported in the unit ball and (d−1)/2 > 1/2 + k, then $$\int_{S^{d-1}} \|\pi_\theta f\|_{C^k}^2\, d\theta \lesssim \|f\|_{L^2}^2.$$ Projection along a random direction θ smooths an function into a C^k function on average.