HaarAveragingScales.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Haar averaging along arbitrarily large good volume scales

theorem OAI.PolycyclicRecognition.haar_averaging_at_unbounded_scales line 17

Source documentation

One sufficiently large good radius for each pair of compact sets is enough; the tripling bound need not hold at every large radius.

theorem haar_averaging_at_unbounded_scales
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    (ℓ : GroupSeminorm G) (hℓ : Measurable ℓ)
    {J : Type*} (E : J → Set G) (a : J → ℝ≥0∞)
    (hE : ∀ j, MeasurableSet (E j))
    (hbounded : ∀ j, ∃ R : ℝ, ∀ e ∈ E j, ℓ e ≤ R)
    {K D : ℝ≥0∞} (hK : K ≠ ∞)
    (hlower : ∀ j z, a j ≤ K * ρ (leftTranslate (E j) z))
    (hupper : ∀ j z, ρ (leftTranslate (E j) z) ≤ K * a j)
    (hballs : ∀ R : ℝ, ∃ T : ℝ, R ≤ T ∧
      μ (lengthBall ℓ T) ≠ 0 ∧ μ (lengthBall ℓ T) ≠ ∞ ∧
…

Mentions: OAI.PolycyclicRecognition.leftTranslate, OAI.PolycyclicRecognition.lengthBall

theorem OAI.PolycyclicRecognition.haar_averaging_compact_at_unbounded_scales line 42

Source documentation

Compact boundary sets admit the same averaging comparison from arbitrarily large radii with a common volume tripling bound.

theorem haar_averaging_compact_at_unbounded_scales
    [MetricSpace G] [BorelSpace G] [IsIsometricSMul G G]
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    {J : Type*} (E : J → Set G) (a : J → ℝ≥0∞)
    (hE : ∀ j, IsCompact (E j)) {K D : ℝ≥0∞} (hK : K ≠ ∞)
    (hlower : ∀ j z, a j ≤ K * ρ (leftTranslate (E j) z))
    (hupper : ∀ j z, ρ (leftTranslate (E j) z) ≤ K * a j)
    (hballs : ∀ R : ℝ, ∃ T : ℝ, R ≤ T ∧
      μ (Metric.ball 1 T) ≠ 0 ∧ μ (Metric.ball 1 T) ≠ ∞ ∧
      μ (Metric.ball 1 (3 * T)) ≤ D * μ (Metric.ball 1 T)) :
    ∀ j k, a j * μ (E k) ≤ (K * K * D) * a k * μ (E j) := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate

theorem OAI.PolycyclicRecognition.haar_averaging_compact_of_polynomial_volume line 70

Source documentation

An upper polynomial volume bound and positivity/finiteness of balls suffice for the compact Haar-averaging comparison.

theorem haar_averaging_compact_of_polynomial_volume
    [MetricSpace G] [BorelSpace G] [IsIsometricSMul G G]
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    {J : Type*} (E : J → Set G) (a : J → ℝ≥0∞)
    (hE : ∀ j, IsCompact (E j)) {K : ℝ≥0∞} (hK : K ≠ ∞)
    (hlower : ∀ j z, a j ≤ K * ρ (leftTranslate (E j) z))
    (hupper : ∀ j z, ρ (leftTranslate (E j) z) ≤ K * a j)
    (hballs : ∀ T : ℝ, 1 ≤ T → μ (Metric.ball 1 T) ≠ 0 ∧ μ (Metric.ball 1 T) ≠ ∞)
    {C : ℝ} (d : ℕ)
    (hvolume : ∀ T : ℝ, 1 ≤ T → (μ (Metric.ball 1 T)).toReal ≤ C * T ^ d) :
    ∀ j k, a j * μ (E k) ≤
…

Mentions: OAI.PolycyclicRecognition.leftTranslate