HaarAveraging.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Averaging translated masses

The boundary argument averages a Radon measure over Haar translates. The identities below use genuine measures and measurable multiplication, including the Tonelli step. Invariance is required only of Haar measure, not of the measure whose translated masses are being compared.

def OAI.PolycyclicRecognition.leftTranslate line 28
Source documentation
A left translate, expressed as a measurable preimage.
```
def leftTranslate (E : Set G) (z : G) : Set G := {y | z⁻¹ * y ∈ E}
…
```
theorem OAI.PolycyclicRecognition.measurableSet_leftTranslate line 31

theorem OAI.PolycyclicRecognition.average_translate_eq line 35

Source documentation

Tonelli's identity for the average mass of translates.

theorem average_translate_eq (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    {E S : Set G} (hE : MeasurableSet E) :
    (∫⁻ z in S, ρ (leftTranslate E z) ∂μ) =
      ∫⁻ y, μ (S ∩ {z | z⁻¹ * y ∈ E}) ∂ρ := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate

theorem OAI.PolycyclicRecognition.translate_kernel_mass line 71

Source documentation

Unimodularity identifies the total mass of the averaging kernel.

theorem translate_kernel_mass (μ : Measure G) [IsInvInvariant μ] [IsMulRightInvariant μ]
    (E : Set G) (y : G) : μ {z | z⁻¹ * y ∈ E} = μ E := by
…

theorem OAI.PolycyclicRecognition.average_translate_sandwich line 79

Source documentation

The set-theoretic sandwich underlying the Haar averaging estimate. inner consists of points whose entire averaging kernel lies in S, while outside outer the kernel misses S.

theorem average_translate_sandwich
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    {E S inner outer : Set G} (hE : MeasurableSet E)
    (hi : MeasurableSet inner) (ho : MeasurableSet outer)
    (hin : ∀ y ∈ inner, ∀ z, z⁻¹ * y ∈ E → z ∈ S)
    (hout : ∀ y, ∀ z ∈ S, z⁻¹ * y ∈ E → y ∈ outer) :
    μ E * ρ inner ≤ (∫⁻ z in S, ρ (leftTranslate E z) ∂μ) ∧
      (∫⁻ z in S, ρ (leftTranslate E z) ∂μ) ≤ μ E * ρ outer := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate

def OAI.PolycyclicRecognition.lengthBall line 115
Source documentation
Balls for a left-invariant length function.
```
def lengthBall (ℓ : GroupSeminorm G) (r : ℝ) : Set G := {x | ℓ x < r}
```
def OAI.PolycyclicRecognition.distanceLength line 119
Source documentation
The group length associated to the left-invariant metric used in the Lie-group application.
```
def distanceLength [PseudoMetricSpace G] [IsIsometricSMul G G] : GroupSeminorm G where
…
```

theorem OAI.PolycyclicRecognition.ball_average_sandwich line 136

Source documentation

The metric version of the Tonelli sandwich. It uses the triangle inequality for group length; commutativity is not required.

theorem ball_average_sandwich
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    (ℓ : GroupSeminorm G) (hℓ : Measurable ℓ)
    {E : Set G} (hE : MeasurableSet E) {R T : ℝ} (hR : ∀ e ∈ E, ℓ e ≤ R) :
    μ E * ρ (lengthBall ℓ (T - R)) ≤
        (∫⁻ z in lengthBall ℓ T, ρ (leftTranslate E z) ∂μ) ∧
      (∫⁻ z in lengthBall ℓ T, ρ (leftTranslate E z) ∂μ) ≤
        μ E * ρ (lengthBall ℓ (T + R)) := by
…

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

theorem OAI.PolycyclicRecognition.average_translate_le line 165

Source documentation

Integrating a uniform upper bound on all translated masses.

theorem average_translate_le (μ ρ : Measure G) {E S : Set G}
    {a K : ℝ≥0∞} (h : ∀ z, ρ (leftTranslate E z) ≤ K * a) :
    (∫⁻ z in S, ρ (leftTranslate E z) ∂μ) ≤ K * a * μ S := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate

theorem OAI.PolycyclicRecognition.le_mul_average_translate line 174

Source documentation

Integrating a uniform lower bound on all translated masses.

theorem le_mul_average_translate (μ ρ : Measure G) {E S : Set G}
    {a K : ℝ≥0∞} (hK : K ≠ ∞) (h : ∀ z, a ≤ K * ρ (leftTranslate E z)) :
    a * μ S ≤ K * (∫⁻ z in S, ρ (leftTranslate E z) ∂μ) := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate

theorem OAI.PolycyclicRecognition.translated_mass_comparison_at_radius line 184

Source documentation

Comparing two compact shapes needs only one finite ball of positive measure and its volume growth bound. The radius may depend on both shapes.

theorem translated_mass_comparison_at_radius
    (μ ρ : Measure G) [SFinite μ] [SFinite ρ]
    [IsInvInvariant μ] [IsMulRightInvariant μ]
    (ℓ : GroupSeminorm G) (hℓ : Measurable ℓ)
    {E F : Set G} (hE : MeasurableSet E) (hF : MeasurableSet F)
    {T : ℝ} (hET : ∀ e ∈ E, ℓ e ≤ T) (hFT : ∀ f ∈ F, ℓ f ≤ T)
    {a b K D : ℝ≥0∞} (hK : K ≠ ∞)
    (ha : ∀ z, a ≤ K * ρ (leftTranslate E z))
    (hb : ∀ z, ρ (leftTranslate F z) ≤ K * b)
    (hvol0 : μ (lengthBall ℓ T) ≠ 0) (hvoltop : μ (lengthBall ℓ T) ≠ ∞)
    (hgrowth : μ (lengthBall ℓ (3 * T)) ≤ D * μ (lengthBall ℓ T)) :
    a * μ F ≤ (K * K * D) * b * μ E := by
…

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

theorem OAI.PolycyclicRecognition.haar_averaging_comparison line 220

Source documentation

The Haar-averaging comparison, uniformly over all bounded measurable shapes. No absolute continuity of ρ is assumed. The growth hypothesis is the large-scale ball-volume bound, independent of the shapes.

theorem haar_averaging_comparison
    (μ ρ : 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 : ∃ T₀ : ℝ, ∀ T, T₀ ≤ T →
      μ (lengthBall ℓ T) ≠ 0 ∧ μ (lengthBall ℓ T) ≠ ∞ ∧
…

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

theorem OAI.PolycyclicRecognition.tripling_of_doubling line 248

Source documentation

A doubling estimate gives the tripling bound used above, with the square of the doubling constant.

theorem tripling_of_doubling (μ : Measure G) (ℓ : GroupSeminorm G)
    {T₀ : ℝ} (hT₀ : 0 ≤ T₀) {D : ℝ≥0∞}
    (hd : ∀ T, T₀ ≤ T → μ (lengthBall ℓ (2 * T)) ≤ D * μ (lengthBall ℓ T))
    {T : ℝ} (hT : T₀ ≤ T) :
    μ (lengthBall ℓ (3 * T)) ≤ (D * D) * μ (lengthBall ℓ T) := by
…

Mentions: OAI.PolycyclicRecognition.lengthBall

theorem OAI.PolycyclicRecognition.haar_averaging_compact line 268

Source documentation

The compact-set version used for boundary images. All geometric inputs are explicit: a left-invariant metric and eventual Haar-volume doubling. The measure ρ can be singular.

theorem haar_averaging_compact
    [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 : ∃ T₀ : ℝ, 0 ≤ T₀ ∧ ∀ T, T₀ ≤ T →
      μ (Metric.ball 1 T) ≠ 0 ∧ μ (Metric.ball 1 T) ≠ ∞ ∧
      μ (Metric.ball 1 (2 * T)) ≤ D * μ (Metric.ball 1 T)) :
    ∀ j k, a j * μ (E k) ≤ (K * K * (D * D)) * a k * μ (E j) := by
…

Mentions: OAI.PolycyclicRecognition.leftTranslate