EndpointTransform.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Original endpoint transforms in arbitrary dimension

The spatial measure argument is already restricted to its cell. A child therefore uses the same endpoint symbol and the original restricted law. The exact finite-measure splitting keeps the model-mass factors explicit.

def OAI.Falconer.endpointTransform line 16
theorem OAI.Falconer.endpoint_integrand_norm line 20
theorem OAI.Falconer.measurable_endpointTransform line 25
theorem OAI.Falconer.endpoint_integrand_integrable line 38
theorem OAI.Falconer.endpointTransform_norm_le line 51

theorem OAI.Falconer.endpointTransform_sum line 64

Source documentation

Exact model-mass splitting of one endpoint transform.

theorem endpointTransform_sum {d : ℕ} {ι : Type*} (S : Finset ι)
    (ρ : ι → Measure (Space d)) [∀ i, IsFiniteMeasure (ρ i)]
    (Ma Mp : ℝ) (hMp : Mp ≠ 0) (b : Space d → Sphere d → ℂ)
    (hb : Measurable (Function.uncurry b)) {C : ℝ} (hC : ∀ x w, ‖b x w‖ ≤ C)
    (r : ℝ) (w : Sphere d) :
    endpointTransform (∑ i ∈ S, ρ i) Ma b r w =
      (Mp / Ma) • ∑ i ∈ S, endpointTransform (ρ i) Mp b r w := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.endpointTransform