CutoffMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.samplingTestedFirstDensity_whole line 11

Source documentation

Exact whole-circle first density, including the retained cutoff.

theorem samplingTestedFirstDensity_whole (b : Bool) (h α s : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    samplingTestedFirstDensity b h α (Set.Icc 0 1) (Set.Icc 0 1) s =
      if b then 1-s else if α ≤ samplingDistance s then 1 else 0 := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.samplingDistance

theorem OAI.FiniteFactor.sampling_diagonal_whole_mass line 25

Source documentation

The exact lost mass of one untested diagonal coordinate is 2α.

theorem sampling_diagonal_whole_mass (h α : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hα1 : α ≤ 1/2) :
    (∫ s, samplingTestedFirstDensity false h α (Set.Icc 0 1) (Set.Icc 0 1) s ∂unitIntervalMeasure) = 1-2*α := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.sourceSampling_cutoff_budget_tendsto line 48
Source documentation
The total cutoff budget tends to zero despite the growing dimension.
```
theorem sourceSampling_cutoff_budget_tendsto :
    Tendsto (fun stage => 2*((sourceSamplingPrefix stage).card : ℝ)*sourceSamplingCutoff stage)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingCutoff
theorem OAI.FiniteFactor.sourceSampling_untested_mass_tendsto line 69
Source documentation
Any subset of untested coordinates retains asymptotically all its mass. The estimate uses its actual varying cardinality, bounded by the prefix.
```
theorem sourceSampling_untested_mass_tendsto (k : ℕ → ℕ)
    (hk : ∀ stage, k stage ≤ (sourceSamplingPrefix stage).card) :
    Tendsto (fun stage => (1-2*sourceSamplingCutoff stage)^(k stage)) atTop (𝓝 1) := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingCutoff