OAI/MeasureTheory/Falconer/Estimates/SphericalEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.sphereMoment line 20
2. theorem OAI.Falconer.sphereMoment_nonneg line 23
3. theorem OAI.Falconer.sphereMoment_measurable line 26
4. theorem OAI.Falconer.sphere_norm_square_integrable line 30
5. theorem OAI.Falconer.sphereMoment_le line 38
6. def OAI.Falconer.independentAngularEnergy line 48
7. theorem OAI.Falconer.independentAngularEnergy_nonneg line 53
8. theorem OAI.Falconer.sphere_product_square_integral line 58
9. theorem OAI.Falconer.angular_product_square_integrable line 66

   Source documentation

   Bounded measurable endpoint transforms give an integrable square on the full radial and independent angular product.

   theorem angular_product_square_integrable {d : ℕ} (v : ℝ) (Ψ : ℝ → ℝ)
       [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)]
       (U V : ℝ × Sphere d → ℂ) (hU : Measurable U) (hV : Measurable V)
       {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
       (hbU : ∀ z, ‖U z‖ ≤ C) (hbV : ∀ z, ‖V z‖ ≤ D) :
       Integrable (fun z : ℝ × (Sphere d × Sphere d) =>
         ‖U (z.1,z.2.1) * V (z.1,z.2.2)‖^2)
         ((PlanarFalconer.sourceAngularShellMeasure v Ψ).prod
           ((sphereMeasure d).prod (sphereMeasure d))) := by
   …

   Mentions: OAI.PlanarFalconer.sourceAngularShellMeasure, OAI.Falconer.Sphere, OAI.Falconer.sphereMeasure

10. theorem OAI.Falconer.independentAngularEnergy_product_integral line 87
11. theorem OAI.Falconer.independentAngularEnergy_graph_schur line 105

    Source documentation

    Schur integration produces precisely the independent child energies defined with the sphere measure in the original ambient dimension.

    theorem independentAngularEnergy_graph_schur {d : ℕ} {ι κ : Type*}
        (a v : ℝ) (Ψ : ℝ → ℝ)
        [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)]
        (S : Finset ι) (K : Finset κ) (G : κ → ι → ι → Prop)
        (U V : ι → ℝ × Sphere d → ℂ)
        (hU : ∀ i ∈ S, Measurable (U i)) (hV : ∀ i ∈ S, Measurable (V i))
        (C D : ι → ℝ) (hC : ∀ i ∈ S, 0 ≤ C i) (hD : ∀ i ∈ S, 0 ≤ D i)
        (hbU : ∀ i ∈ S, ∀ z, ‖U i z‖ ≤ C i) (hbV : ∀ i ∈ S, ∀ z, ‖V i z‖ ≤ D i)
        (weight : κ → ℝ × (Sphere d × Sphere d) → ℝ) (degree : ℝ)
        (hweight : ∀ z k, k ∈ K → 0 ≤ weight k z)
        (hpartition : ∀ z, ∑ k ∈ K, weight k z = 1)
        (hrow : ∀ k ∈ K, ∀ i ∈ S, ((S.filter (G k i)).card : ℝ) ≤ degree)
    …

    Mentions: OAI.PlanarFalconer.sourceAngularShellMeasure, OAI.Falconer.Sphere