ConeOffsetPacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The offset inequality from actual lifted cells and section volumes

The first-sheet quotient restriction and the second-sheet ideal restriction bound all lifted cells. The tile count and source count then cancel their template exponents, leaving the sign of the quotient trace.

theorem OAI.PolycyclicRecognition.card_le_real_finite_cover line 22

Source documentation

The covering need not partition the endpoints, and empty tiles are allowed. A common real cardinal bound still sums over the finite cover.

theorem card_le_real_finite_cover {G : Type*} {k : ℕ}
    (s : Finset G) (t : Fin k → Finset G)
    (hcover : ∀ x ∈ s, ∃ j, x ∈ t j) {B : ℝ}
    (hbound : ∀ j, ((t j).card : ℝ) ≤ B) :
    (s.card : ℝ) ≤ (k : ℝ) * B := by
…

theorem OAI.PolycyclicRecognition.cone_offset_nonpos_of_lifted_cells line 50

Source documentation

This is the geometric counting endgame: restrictions on actual quotient and ideal coordinates imply the offset trace inequality. No point-count estimate or offset-sign assertion is assumed.

theorem cone_offset_nonpos_of_lifted_cells
    (π : N →* Q) (hπ : Continuous π) (σ : C(Q, N))
    (hs : ∀ q, π (σ q) = q)
    (μQ : Measure Q) (μI : Measure π.ker) (μ : Measure N) (ν : Measure D)
    [SFinite μQ] [SFinite μI] [SFinite μ] [SFinite ν]
    [μQ.IsMulLeftInvariant] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    (hμ : μ = Measure.map (quotientSectionHomeomorph π hπ σ hs).symm
      (μQ.prod μI))
    (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
…

Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph