CapTransport.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Transport of cap bounds from auxiliary projections

The fixed factor in the cap radius can be absorbed in an arbitrarily small power of the resolution. The center of an original cap need not be in the domain where normalized projection is Lipschitz; we choose an actual source direction in a nonempty cap, and double its radius before projecting. This is the lifting step of prep:integer-caps.

theorem OAI.Falconer.radial_ne_diagonal line 21
theorem OAI.Falconer.projected_radial_identity line 29
theorem OAI.Falconer.projected_radial_norm line 35

theorem OAI.Falconer.projected_radial_cap line 43

Source documentation

Every actual direction in an original radius-u cap maps into a radius max 1 (4/c) * u cap about any chosen actual direction in the first cap.

theorem projected_radial_cap {d k : ℕ} (P : Space d →L[ℝ] Space k)
    {x y y₀ w : Space d} {c u : ℝ} (hc : 0 < c) (hP : ‖P‖ ≤ 1)
    (hy : c ≤ ‖P (radialDirection x y)‖)
    (hy₀ : c ≤ ‖P (radialDirection x y₀)‖)
    (hcap : dist (radialDirection x y) w < u)
    (hcap₀ : dist (radialDirection x y₀) w < u) :
    dist (radialDirection (P x) (P y)) (radialDirection (P x) (P y₀)) <
      max 1 (4 / c) * u := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection

theorem OAI.Falconer.eventually_radius_factor_absorbed line 68
Source documentation
A fixed radius enlargement is absorbed into the permitted scale loss.
```
theorem eventually_radius_factor_absorbed {K q a : ℝ} (ha : 0 < a) :
    ∀ᶠ N : ℕ in atTop, K ^ q ≤ ((2 : ℝ) ^ N) ^ a := by
…
```
theorem OAI.Falconer.enlarged_cap_scalar line 74

theorem OAI.Falconer.projected_fiber_cap_bound line 86

Source documentation

A cap estimate for the projected source law bounds a fiber of the original law. Source labels remain distinct even when their images coincide.

theorem projected_fiber_cap_bound {d k : ℕ} (P : Space d →L[ℝ] Space k)
    (ν : ProbabilityMeasure (Space d)) (H : Set (Space d)) (J : Set (Space k))
    (x : Space d) {R c e a q : ℝ}
    (hR : 1 ≤ R) (hc : 0 < c) (hP : ‖P‖ ≤ 1) (he : 0 ≤ e) (hq : 0 ≤ q)
    (hconstant : (max 1 (4 / c)) ^ q ≤ R ^ a)
    (himage : ∀ y ∈ H, P y ∈ J)
    (hlower : ∀ y ∈ H, c ≤ ‖P (radialDirection x y)‖)
    (hcap : ∀ w : Space k, ‖w‖ = 1 → ∀ u : ℝ, R⁻¹ ≤ u → u ≤ 1 →
      ((ν.map P : ProbabilityMeasure (Space k)) : Measure (Space k))
        {y | y ∈ J ∧ dist (radialDirection (P x) y) w < u} ≤
          ENNReal.ofReal (R ^ e * u ^ q)) :
    ∀ w : Space d, ‖w‖ = 1 → ∀ u : ℝ, R⁻¹ ≤ u → u ≤ 1 →
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection

theorem OAI.Falconer.map_mem_support line 130

theorem OAI.Falconer.RadialCapBound.pullback line 141

Source documentation

Pull back both cap estimates through a fixed auxiliary projection.

theorem RadialCapBound.pullback {d k N : ℕ} (P : Space d →L[ℝ] Space k)
    (μ ν : ProbabilityMeasure (Space d))
    {G : Set (Space d × Space d)} {G' : Set (Space k × Space k)} {c e a q : ℝ}
    (hc : 0 < c) (hP : ‖P‖ ≤ 1) (he : 0 ≤ e) (hq : 0 ≤ q)
    (hconstant : (max 1 (4 / c)) ^ q ≤ ((2 : ℝ) ^ N) ^ a)
    (hG : G ⊆ Prod.map P P ⁻¹' G')
    (hlower : ∀ z ∈ G, c ≤ ‖P (radialDirection z.1 z.2)‖ ∧
      c ≤ ‖P (radialDirection z.2 z.1)‖)
    (hcap : RadialCapBound (μ.map P) (ν.map P) G' N e q) :
    RadialCapBound μ ν G N (e + a) q := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection, OAI.Falconer.RadialCapBound

theorem OAI.Falconer.CapAvailable.pullback line 167

Source documentation

Auxiliary projected cap estimates lift to the original pair law. The deletion is the preimage of the projected bad set intersected with the original pair filter; its mass is bounded by the projected product mass.

theorem CapAvailable.pullback {d k : ℕ} (P : Space d →L[ℝ] Space k)
    (μ ν : ProbabilityMeasure (Space d))
    {Γ : ℕ → Set (Space d × Space d)} {Γ' : ℕ → Set (Space k × Space k)} {c q : ℝ}
    (hc : 0 < c) (hP : ‖P‖ ≤ 1) (hq : 0 ≤ q)
    (hΓ : ∀ N, MeasurableSet (Γ N))
    (hΓsub : ∀ N, Γ N ⊆ Prod.map P P ⁻¹' Γ' N)
    (hlower : ∀ N, ∀ z ∈ Γ N, c ≤ ‖P (radialDirection z.1 z.2)‖ ∧
      c ≤ ‖P (radialDirection z.2 z.1)‖)
    (hcap : CapAvailable (μ.map P) (ν.map P) Γ' q) :
    CapAvailable μ ν Γ q := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.radialDirection, OAI.Falconer.CapAvailable