QuotientSectionVolume.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Volume bounds at arbitrary translated quotient locations

The admissible set only needs separate bounds on its ideal and quotient coordinates. Its coordinates need not be independent or form a product.

theorem OAI.PolycyclicRecognition.quotientSection_measure_le line 29
Source documentation
Separate coordinate restrictions bound the actual pushed-forward measure by the measure of the containing product set.
```
theorem quotientSection_measure_le (E : Set N) (T : Set Q) (B : Set π.ker)
    (hE : ∀ n ∈ E, π n ∈ T ∧ quotientSectionResidual π s hs n ∈ B) :
    (Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI)) E ≤
      μQ T * μI B := by
…
```
Mentions: OAI.PolycyclicRecognition.quotientSectionResidual, OAI.PolycyclicRecognition.quotientSectionHomeomorph

theorem OAI.PolycyclicRecognition.quotientSection_translated_measure_le line 47

Source documentation

A left translate contributes no extra quotient volume, even if the translated set is arbitrarily far from the identity.

theorem quotientSection_translated_measure_le [μQ.IsMulLeftInvariant]
    (E : Set N) (T : Set Q) (B : Set π.ker) (q₀ : Q) (α : Q ≃ Q)
    (J : ℝ≥0∞) (hα : μQ (α '' T) = J * μQ T)
    (hE : ∀ n ∈ E, π n ∈ q₀ • (α '' T) ∧ quotientSectionResidual π s hs n ∈ B) :
    (Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI)) E ≤
      J * μQ T * μI B := by
…

Mentions: OAI.PolycyclicRecognition.quotientSectionResidual, OAI.PolycyclicRecognition.quotientSectionHomeomorph

theorem OAI.PolycyclicRecognition.quotientSection_translated_real_volume_le line 59

Source documentation

The same bound in real Haar volume, with the exact exponential multiplier. Finiteness is needed only to pass from extended real volume.

theorem quotientSection_translated_real_volume_le [μQ.IsMulLeftInvariant]
    (E : Set N) (T : Set Q) (B : Set π.ker) (q₀ : Q) (α : Q ≃ Q)
    (d : ℝ) (hα : μQ (α '' T) = ENNReal.ofReal (Real.exp d) * μQ T)
    (hT : μQ T ≠ ⊤) (hB : μI B ≠ ⊤)
    (hE : ∀ n ∈ E, π n ∈ q₀ • (α '' T) ∧ quotientSectionResidual π s hs n ∈ B) :
    ((Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI)) E).toReal ≤
      Real.exp d * (μQ T).toReal * (μI B).toReal := by
…

Mentions: OAI.PolycyclicRecognition.quotientSectionResidual, OAI.PolycyclicRecognition.quotientSectionHomeomorph