OAI/Analysis/FiniteFactor/OrbitSampling/RectangleError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_integral_square_le line 12

   Source documentation

   The elementary probability-space Cauchy--Schwarz bound, proved by integrating the nonnegative square centered at the mean.

   theorem sampling_integral_square_le {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ)
       (hf : Integrable f μ) (hf2 : Integrable (fun x => f x^2) μ) :
       (∫ x, f x ∂μ)^2 ≤ ∫ x, f x^2 ∂μ := by
   …

2. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_rectangle_mass line 29

   Source documentation

   Actual rectangle mass equals the integral of the first tested empirical density at every admissible stage.

   theorem sourceSamplingUntrimmed_rectangle_mass (I : Finset SourceCoordinate) (stage : ℕ)
       (E G : SourceCoordinate → Set ℝ)
       (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (houtside : ∀ i ∉ sourceSamplingPrefix stage,
         Set.Ico (0 : ℝ) 1 ⊆ E i ∧ Set.Ico (0 : ℝ) 1 ⊆ G i)
       (θ : SourceCoordinate → ℝ) :
       ((sourceSamplingUntrimmed I stage θ) (sourceSamplingRectangle E G)).toReal =
         ∫ x, sourceSamplingEmpiricalDensity stage false (fun i => decide (i ∈ I)) E G θ x
           ∂sourceSamplingHaar := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.sourceSamplingHaar

3. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_rectangle_error line 54

   Source documentation

   Full squared sampling error bounds the squared discrepancy of the actual rectangle mass and the ideal product integral.

   theorem sourceSamplingUntrimmed_rectangle_error (I : Finset SourceCoordinate) (stage : ℕ)
       (E G : SourceCoordinate → Set ℝ)
       (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
       (houtside : ∀ i ∉ sourceSamplingPrefix stage,
         Set.Ico (0 : ℝ) 1 ⊆ E i ∧ Set.Ico (0 : ℝ) 1 ⊆ G i)
       (θ : SourceCoordinate → ℝ) :
       (((sourceSamplingUntrimmed I stage θ) (sourceSamplingRectangle E G)).toReal -
         ∫ x, sourceSamplingIdealDensity stage false (fun i => decide (i ∈ I)) E G x ∂sourceSamplingHaar)^2 ≤
       sourceSamplingSquaredError stage false (fun i => decide (i ∈ I)) E G θ := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceSamplingSquaredError