FilteredLimit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Limits of decreasing original-pair filters

For the manuscript application, ρ is the original product measure with the bounded distance weight, and f is the original distance map. These lemmas do not replace distances by those of any auxiliary projection.

def OAI.Falconer.filteredPushforward line 21
theorem OAI.Falconer.filteredPushforward_mono line 24
theorem OAI.Falconer.filteredPushforward_mass line 29
instance OAI.Falconer.filteredPushforward_finite line 34

theorem OAI.Falconer.antitone_filteredPushforward line 39

Source documentation

Decreasing filters produce a decreasing sequence of pushforwards.

theorem antitone_filteredPushforward (f : X → Y) (hf : Measurable f)
    (ρ : Measure X) {G : ℕ → Set X} (hG : Antitone G) :
    Antitone (fun n => filteredPushforward f ρ (G n)) := by
…

Mentions: OAI.Falconer.filteredPushforward

theorem OAI.Falconer.filteredPushforward_tail_mass_tendsto line 47

Source documentation

Continuity from above gives convergence in the mass of the positive remaining tail; it supplies no quantitative convergence rate.

theorem filteredPushforward_tail_mass_tendsto (f : X → Y) (hf : Measurable f)
    (ρ : Measure X) [IsFiniteMeasure ρ] (G : ℕ → Set X)
    (hG : ∀ n, MeasurableSet (G n)) (hmono : Antitone G) :
    Tendsto (fun n => (filteredPushforward f ρ (G n) -
      filteredPushforward f ρ (⋂ j, G j)).real univ) atTop (𝓝 0) := by
…

Mentions: OAI.Falconer.filteredPushforward

theorem OAI.Falconer.filteredPushforward_positive line 68
Source documentation
Positive retained weighted mass remains positive after distance pushforward.
```
theorem filteredPushforward_positive (f : X → Y) (hf : Measurable f)
    (ρ : Measure X) {G : Set X} (hG : 0 < ρ G) :
    0 < filteredPushforward f ρ G univ := by
…
```
Mentions: OAI.Falconer.filteredPushforward

theorem OAI.Falconer.filteredPushforward_carried line 74

Source documentation

Restriction preserves the carrier of the original pushforward.

theorem filteredPushforward_carried (f : X → Y) (hf : Measurable f)
    (ρ : Measure X) (G : Set X) {D : Set Y} (hD : MeasurableSet D)
    (hcarry : ρ (f ⁻¹' Dᶜ) = 0) : filteredPushforward f ρ G Dᶜ = 0 := by
…

Mentions: OAI.Falconer.filteredPushforward