Availability.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Available radial exponents in the original product measure

These definitions record prep:availability. A bad set is a measurable set of original pairs, and each remaining radial fiber is measured using the original opposite marginal. No fiber is renormalized. The closure and bootstrap express parts of prep:thin-upgrade.

def OAI.Falconer.radialDirection line 24
Source documentation
Radial direction, assigned zero on the diagonal. The application uses separated supports, so this arbitrary diagonal value has no effect.
```
noncomputable def radialDirection {d : ℕ} (x y : Space d) : Space d :=
…
```
Mentions: OAI.Falconer.Space
def OAI.Falconer.RadialCapBound line 28
Source documentation
Both directional cap estimates, using the original opposite probability.
```
def RadialCapBound {d : ℕ} (μ ν : ProbabilityMeasure (Space d))
    (G : Set (Space d × Space d)) (N : ℕ) (e q : ℝ) : Prop :=
…
```
Mentions: OAI.Falconer.Space
def OAI.Falconer.CapAvailable line 41
Source documentation
A radial cap exponent available after a power-small deletion of original pairs. Constants and the starting scale may depend on the desired loss.
```
def CapAvailable {d : ℕ} (μ ν : ProbabilityMeasure (Space d))
    (Γ : ℕ → Set (Space d × Space d)) (q : ℝ) : Prop :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.cap_power_change line 50
theorem OAI.Falconer.cap_bound_change line 59
theorem OAI.Falconer.RadialCapBound.change_exponent line 70

theorem OAI.Falconer.RadialCapBound.mono line 84

Source documentation

Restricting a pair relation can only decrease each original radial fiber.

theorem RadialCapBound.mono {d N : ℕ} {μ ν : ProbabilityMeasure (Space d)}
    {G H : Set (Space d × Space d)} {e q : ℝ}
    (h : RadialCapBound μ ν G N e q) (hHG : H ⊆ G) :
    RadialCapBound μ ν H N e q := by
…

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

theorem OAI.Falconer.CapAvailable.restrict line 105
Source documentation
Integer cap bounds continue to hold after the coarse pair filters of prep:coarse-filter are imposed. Only the original bad pairs still lying inside the new filter need to be deleted.
```
theorem CapAvailable.restrict {d : ℕ} {μ ν : ProbabilityMeasure (Space d)}
    {Γ Γ' : ℕ → Set (Space d × Space d)} {q : ℝ}
    (hq : CapAvailable μ ν Γ q) (hΓ' : ∀ N, MeasurableSet (Γ' N))
    (hsub : ∀ N, Γ' N ⊆ Γ N) : CapAvailable μ ν Γ' q := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.CapAvailable

theorem OAI.Falconer.CapAvailable.mono line 120

Source documentation

Decreasing the requested cap exponent needs no additional deletion.

theorem CapAvailable.mono {d : ℕ} {μ ν : ProbabilityMeasure (Space d)}
    {Γ : ℕ → Set (Space d × Space d)} {q q' : ℝ}
    (hq : CapAvailable μ ν Γ q) (hqq : q' ≤ q) : CapAvailable μ ν Γ q' := by
…

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

theorem OAI.Falconer.isClosed_capAvailable line 134
Source documentation
The allowance of every positive scale loss makes availability closed in the exponent. The same original bad sets and deletion rates work after the small exponent change.
```
theorem isClosed_capAvailable {d : ℕ} (μ ν : ProbabilityMeasure (Space d))
    (Γ : ℕ → Set (Space d × Space d)) :
    IsClosed {q : ℝ | CapAvailable μ ν Γ q} := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.CapAvailable

theorem OAI.Falconer.capAvailable_half_integer line 153

Source documentation

The thin-tube endpoint follows from the integer starting exponent and the one-scale strict improvement, using closure of cap availability.

theorem capAvailable_half_integer {d : ℕ} (k : ℕ)
    (μ ν : ProbabilityMeasure (Space d)) (Γ : ℕ → Set (Space d × Space d))
    (hstart : CapAvailable μ ν Γ ((k : ℝ) - 1))
    (himprove : ∀ q : ℝ, (k : ℝ) - 1 ≤ q → q < (k : ℝ) - 1 / 2 →
      CapAvailable μ ν Γ q →
      ∃ q' : ℝ, q < q' ∧ q' ≤ (k : ℝ) - 1 / 2 ∧ CapAvailable μ ν Γ q') :
    CapAvailable μ ν Γ ((k : ℝ) - 1 / 2) := by
…

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