TailTrimming.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.unitInterval_order_failure line 11
def OAI.FiniteFactor.sourceTailOrderFailure line 20
theorem OAI.FiniteFactor.SourceAngles.block_sum_le line 24
theorem OAI.FiniteFactor.SourceAngles.tail_block_summable line 34
theorem OAI.FiniteFactor.SourceAngles.tail_order_probability line 44
Source documentation
Actual Haar probability of violating order in any tail coordinate, for one positive orbit power. The countably infinite union is controlled.
```
theorem SourceAngles.tail_order_probability {θ : SourceCoordinate → ℝ} (hθ : SourceAngles θ) (s n : ℕ) :
    (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure))
      (sourceTailOrderFailure θ s n) ≤ ENNReal.ofReal (4*(n : ℝ)/((sourceStageState s).K : ℝ)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceTailOrderFailure, OAI.FiniteFactor.sourceStageState
theorem OAI.FiniteFactor.sourceSampling_tail_error_tendsto line 87
Source documentation
The source's trimming error tends to zero for every admissible angle realization, uniformly for all positive powers up to Q_s=m_s^((7/10)m_s).
```
theorem sourceSampling_tail_error_tendsto :
    Tendsto (fun s => 4*(sourceBlockSize s : ℝ)^(-(sourceBlockSize s : ℝ)/20)) atTop (𝓝 0) := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize