WeightedTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSampling_weighted_tail_loss line 14
Source documentation
The actual prefix-weighted summand loses at most the source tail budget relative to its own mass. Coordinate independence is applied before the countable union bound; a Haar estimate alone would not prove this statement.
```
theorem sourceSampling_weighted_tail_loss (I : Finset SourceCoordinate) (s : ℕ)
    (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (n : ℕ) :
    sourceSamplingWeightedMeasure I s θ (n : ℤ) (sourceTailOrderFailure θ (s+1) n) ≤
      sourceSamplingWeightedMeasure I s θ (n : ℤ) Set.univ *
        ENNReal.ofReal (4*(n : ℝ)/((sourceStageState (s+1)).K : ℝ)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceSamplingWeightedMeasure, OAI.FiniteFactor.sourceTailOrderFailure, OAI.FiniteFactor.sourceStageState

theorem OAI.FiniteFactor.sourceSampling_weighted_tail_small line 61

Source documentation

The source exponent gap now bounds actual weighted lost mass, uniformly for every positive power at most Q.

theorem sourceSampling_weighted_tail_small (I : Finset SourceCoordinate) (s : ℕ)
    (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (n : ℕ)
    (hn : (n : ℝ) ≤ samplingQ (sourceBlockSize s)) :
    sourceSamplingWeightedMeasure I s θ (n : ℤ) (sourceTailOrderFailure θ (s+1) n) ≤
      sourceSamplingWeightedMeasure I s θ (n : ℤ) Set.univ *
        ENNReal.ofReal (4*(sourceBlockSize s : ℝ)^(-(sourceBlockSize s : ℝ)/20)) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.samplingQ, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceSamplingWeightedMeasure, OAI.FiniteFactor.sourceTailOrderFailure