EnergySplitting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact independent-energy expansion on the original dyadic cells

The two endpoint laws and their symbols are unchanged when passing to occupied descendants. The identity keeps every complex cross term inside the angular--radial integral, where nonstationary localization is applied.

abbrev OAI.Falconer.angularProductMeasure line 17
theorem OAI.Falconer.complex_sum_square line 21
theorem OAI.Falconer.integral_cross_sum_norm line 28
def OAI.Falconer.dyadicPairTransform line 39
theorem OAI.Falconer.dyadicPairTransform_sum line 47

theorem OAI.Falconer.independentAngularEnergy_dyadic_expansion line 68

Source documentation

Exact expansion before any cross term is discarded or replaced by its absolute value. The child masses are the chosen model masses.

theorem independentAngularEnergy_dyadic_expansion {d : ℕ} (Q₁ Q₂ : DyadicCube d)
    (μ ν : Measure (Space d)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (n : ℕ) (a v : ℝ) (Ψ : ℝ → ℝ)
    [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)]
    (Ma₁ Ma₂ Mp₁ Mp₂ : ℝ) (hMa₁ : 0 < Ma₁) (hMa₂ : 0 < Ma₂)
    (hMp₁ : Mp₁ ≠ 0) (hMp₂ : Mp₂ ≠ 0)
    (b c : Space d → Sphere d → ℂ)
    (hb : Measurable (Function.uncurry b)) (hc : Measurable (Function.uncurry c))
    {B C : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C)
    (hbB : ∀ x w, ‖b x w‖ ≤ B) (hcC : ∀ x w, ‖c x w‖ ≤ C) :
    independentAngularEnergy a v Ψ
      (fun z => endpointTransform (μ.restrict Q₁.carrier) Ma₁ b z.1 z.2)
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.PlanarFalconer.sourceAngularShellMeasure, OAI.Falconer.Sphere, OAI.Falconer.independentAngularEnergy, OAI.Falconer.endpointTransform