EmpiricalL2.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingEmpiricalDensity_measurable line 10
theorem OAI.FiniteFactor.sourceSamplingEmpiricalDensity_bounds line 18
Source documentation
Every empirical density is bounded at its finite stage, including stages whose selected set is empty. No asymptotic assumption is used here.
```
theorem sourceSamplingEmpiricalDensity_bounds (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
    (E G : SourceCoordinate → Set ℝ) (θ x : SourceCoordinate → ℝ) :
    0 ≤ sourceSamplingEmpiricalDensity stage r b E G θ x ∧
      sourceSamplingEmpiricalDensity stage r b E G θ x ≤
        (max 1 (1/(sourceSamplingWidth stage*sourceSamplingCutoff stage)))^(sourceSamplingPrefix stage).card := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceSamplingPrefix

theorem OAI.FiniteFactor.sourceSamplingEmpiricalDensity_memLp line 39

Source documentation

The empirical densities, not only the ideal products, belong to L2.

theorem sourceSamplingEmpiricalDensity_memLp (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
    (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
    (θ : SourceCoordinate → ℝ) :
    MemLp (sourceSamplingEmpiricalDensity stage r b E G θ) 2
      (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.sourceSamplingEmpiricalDensity_square_le line 52

Source documentation

The full error and the ideal L2 bound control the actual empirical square.

theorem sourceSamplingEmpiricalDensity_square_le (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
    (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
    (θ : SourceCoordinate → ℝ) :
    (∫ x, sourceSamplingEmpiricalDensity stage r b E G θ x^2
      ∂Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) ≤
      2*sourceSamplingSquaredError stage r b E G θ+2*Real.exp 5 := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceSamplingSquaredError