FixedSlicePacking.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Lower packing on a fixed Cartan slice

A finite net in the ambient group pulls back to a cover of the nilpotent parameter set. Conjugation preserving Haar makes the mass of every pulled-back ball independent of the slice position. This is the fixed-position part of the manuscript's lower packing argument, with no assumption on an image's absolute continuity or multiplicity.

theorem OAI.PolycyclicRecognition.exists_separated_image_net_volume_bound line 25

Source documentation

A net of an image gives a lower cardinality bound whenever the preimage of each covering ball has uniformly bounded mass. The source set need not be measurable.

theorem exists_separated_image_net_volume_bound
    {N G : Type*} [MeasurableSpace N] [PseudoMetricSpace G]
    (μ : Measure N) (f : N → G) {S : Set N}
    (hS : TotallyBounded (f '' S)) {r : ℝ} (hr : 0 < r) (C : ℝ≥0∞)
    (hball : ∀ y ∈ f '' S, μ (f ⁻¹' closedBall y r) ≤ C) :
    ∃ t : Finset G, (↑t : Set G) ⊆ f '' S ∧
      (∀ x ∈ t, ∀ y ∈ t, x ≠ y → r < dist x y) ∧
      μ S ≤ (t.card : ℝ≥0∞) * C := by
…

theorem OAI.PolycyclicRecognition.fixedSlice_ball_preimage line 52

Source documentation

Compute the entire fiber of an ambient ball on a fixed slice. The identity-neighborhood in the nilpotent group is conjugated, then translated.

theorem fixedSlice_ball_preimage
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (x : G) (d : D) (v : N) (r : ℝ) :
    (fun u : N => x * ι u * κ d) ⁻¹' closedBall (x * ι v * κ d) r =
      (fun n => v * φ d n) '' (ι ⁻¹' closedBall (1 : G) r) := by
…

theorem OAI.PolycyclicRecognition.fixedSlice_ball_measure line 93

Source documentation

Haar mass of a slice ball depends only on its radius. In particular it does not grow with the Cartan position or the center of the ball.

theorem fixedSlice_ball_measure
    (μ : Measure N) [μ.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (x : G) (d : D) (v : N) (r : ℝ) :
    μ ((fun u : N => x * ι u * κ d) ⁻¹' closedBall (x * ι v * κ d) r) =
      μ (ι ⁻¹' closedBall (1 : G) r) := by
…

theorem OAI.PolycyclicRecognition.exists_fixedSlice_separated_net line 117

Source documentation

The fixed-position lower packing estimate. The only volume constant is the Haar mass of the identity ball pulled back to the nilpotent subgroup.

theorem exists_fixedSlice_separated_net
    (μ : Measure N) [μ.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (x : G) (d : D) (S : Set N)
    (hS : TotallyBounded ((fun u : N => x * ι u * κ d) '' S))
    {r : ℝ} (hr : 0 < r) :
    ∃ t : Finset G, (↑t : Set G) ⊆ (fun u : N => x * ι u * κ d) '' S ∧
      (∀ a ∈ t, ∀ b ∈ t, a ≠ b → r < dist a b) ∧
      μ S ≤ (t.card : ℝ≥0∞) * μ (ι ⁻¹' closedBall (1 : G) r) := by
…

theorem OAI.PolycyclicRecognition.fixedSlice_packing_constant_lt_top line 136

Source documentation

A closed subgroup realization gives a finite packing constant at every fixed radius, since the ambient metric is proper.

theorem fixedSlice_packing_constant_lt_top
    [ProperSpace G] (μ : Measure N) [IsFiniteMeasureOnCompacts μ]
    (hι : Topology.IsClosedEmbedding ι) (r : ℝ) :
    μ (ι ⁻¹' closedBall (1 : G) r) < ⊤ :=
…

theorem OAI.PolycyclicRecognition.exists_fixedSlice_separated_net_of_compact line 144

Source documentation

Any subset of a compact parameter set satisfies the fixed-slice lower packing bound. Its image need not be measurable.

theorem exists_fixedSlice_separated_net_of_compact
    (μ : Measure N) [μ.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (hι : Continuous ι) (x : G) (d : D) {K S : Set N}
    (hK : IsCompact K) (hS : S ⊆ K) {r : ℝ} (hr : 0 < r) :
    ∃ t : Finset G, (↑t : Set G) ⊆ (fun u : N => x * ι u * κ d) '' S ∧
      (∀ a ∈ t, ∀ b ∈ t, a ≠ b → r < dist a b) ∧
      μ S ≤ (t.card : ℝ≥0∞) * μ (ι ⁻¹' closedBall (1 : G) r) := by
…