MeasuredProbeRegions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The measured regions produced by the two-path construction

structure OAI.PolycyclicRecognition.MeasuredProbeRegions line 17

Source documentation

One section and three containing regions, with their actual measure bounds. The ideal exponent is fixed while the loss is subexponential.

structure MeasuredProbeRegions {N D Q : Type*} [Group N] [Group Q]
    [TopologicalSpace N] [TopologicalSpace Q]
    [MeasurableSpace Q] [MeasurableSpace N] [MeasurableSpace D]
    (π : N →* Q) (μQ : Measure Q) (μI : Measure π.ker) (ν : Measure D)
    (scale : ℕ → ℝ) (P : ℝ) where
…

def OAI.PolycyclicRecognition.MeasuredProbeRegions.ControlsTwoPaths line 49
Source documentation
The path property proved for the measured regions. This records geometric input paths and the single fixed lift controlling the whole right cell, without choosing points or tile frames.
```
def MeasuredProbeRegions.ControlsTwoPaths
    (R : MeasuredProbeRegions π μQ μI ν scale P)
    (project : N → D → G) (φ : D →* MulAut N) (act : G → Q → Q)
    (height : G →* Multiplicative W) (cell : Set (N × D))
    (E₁ E₂ : Set W) (η : ℕ → ℝ) (A B δ : ℝ) (n : ℕ) : Prop :=
…
```
Mentions: OAI.PolycyclicRecognition.MeasuredProbeRegions