OAI/GroupTheory/PolycyclicRecognition/Analysis/ProbeAnchorHaarBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.anchor_height_error_of_affine_profiles line 16

   Source documentation

   At the common pivot, the linear parts cancel across the two sheets. The actual anchor-to-base height has the sign needed for quotient volume.

   theorem anchor_height_error_of_affine_profiles
       {G W V Z : Type*} [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
       [AddCommGroup V] [Module ℝ V]
       (π : G →* Multiplicative W) (F : G → G) (x base anchor : G)
       (r : ℝ) (φ : Z → G) (q : Z → V) (A : V →ₗ[ℝ] W)
       (b₁ b₂ : W) (z₀ : Z) {ε₁ ε₂ : ℝ}
       (hbase : ‖rescaledMapProfile (fun g => (π (F g)).toAdd) x base r φ z₀ -
         (A (q z₀) + b₁)‖ ≤ ε₁)
       (hanchor : ‖rescaledMapProfile (fun g => (π (F g)).toAdd) x anchor r φ z₀ -
         (A (q z₀) + b₂)‖ ≤ ε₂) :
       ‖(π ((F (x * anchor * φ z₀))⁻¹ * F (x * base * φ z₀))).toAdd +
         Real.exp r • (b₂ - b₁)‖ ≤ Real.exp r * (ε₁ + ε₂) := by
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

2. theorem OAI.PolycyclicRecognition.anchor_haar_bound_of_affine_profiles line 39

   Source documentation

   The profile estimate supplies the Haar bound uniformly over any finite or infinite family of anchors. The quotient set may vary with the scale.

   theorem anchor_haar_bound_of_affine_profiles
       {G Q W V Z : Type*} [Group G] [MeasurableSpace Q]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [AddCommGroup V] [Module ℝ V]
       (π : G →* Multiplicative W) (F : G → G) (x base anchor : G)
       (r : ℝ) (φ : Z → G) (q : Z → V) (A : V →ₗ[ℝ] W)
       (b₁ b₂ : W) (z₀ : Z) {ε₁ ε₂ : ℝ}
       (hbase : ‖rescaledMapProfile (fun g => (π (F g)).toAdd) x base r φ z₀ -
         (A (q z₀) + b₁)‖ ≤ ε₁)
       (hanchor : ‖rescaledMapProfile (fun g => (π (F g)).toAdd) x anchor r φ z₀ -
         (A (q z₀) + b₂)‖ ≤ ε₂)
       (ell : W →L[ℝ] ℝ) (μ : Measure Q) (α : Q ≃ Q) (S : Set Q)
       (hvol : μ (α '' S) = ENNReal.ofReal (Real.exp (ell
   …

   Mentions: OAI.PolycyclicRecognition.rescaledMapProfile