Eligibility.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Eligible cell--cap incidences

Positive incidence supplies one point--angle witness. Zero incidence annihilates the endpoint transform on almost every angle in the cap, simultaneously for every radial frequency. The symbols need only be measurable in the spatial variable.

def OAI.Falconer.capIncidence line 17
theorem OAI.Falconer.capIncidence_witness line 21
theorem OAI.Falconer.endpoint_square_integrable line 35
theorem OAI.Falconer.endpoint_square_le line 45

theorem OAI.Falconer.capIncidence_zero_transform line 58

Source documentation

A null cell--cap incidence is removed as an integrated whole. There is no frequency-dependent exceptional set of angles.

theorem capIncidence_zero_transform {d : ℕ} (ρ : Measure (Space d)) [IsFiniteMeasure ρ]
    (η : Sphere d → ℝ) (hηm : Measurable η) (hη : ∀ w, 0 ≤ η w)
    (b : Space d → Sphere d → ℂ) (hb : Measurable (Function.uncurry b))
    {B C : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C)
    (hηB : ∀ w, η w ≤ B) (hbound : ∀ x w, ‖b x w‖ ≤ C)
    (hzero : capIncidence ρ η b = 0) (M : ℝ) :
    ∀ᵐ w ∂sphereMeasure d, 0 < η w → ∀ r, endpointTransform ρ M b r w = 0 := by
…

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

theorem OAI.Falconer.capIncidence_zero_weightedIntegral line 93