OAI/Analysis/FiniteFactor/OrbitSampling/RationalTests.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceSamplingRationalTest line 13

   Source documentation

   A finite rational cylinder test, with two closed intervals per tested coordinate. Whole-circle tests fill the remaining coordinates.

   abbrev SourceSamplingRationalTest :=
   …

2. instance OAI.FiniteFactor.(instance at line 16) line 16
3. def OAI.FiniteFactor.sourceSamplingRationalEndpoints line 18
4. def OAI.FiniteFactor.sourceSamplingRationalX line 22
5. def OAI.FiniteFactor.sourceSamplingRationalY line 25
6. theorem OAI.FiniteFactor.sourceSamplingRationalTests_outside line 28
7. theorem OAI.FiniteFactor.sourceSamplingPrefix_eventually_covers line 39
8. theorem OAI.FiniteFactor.sourceSampling_rational_event line 49

   Source documentation

   A concrete single conull event for every finite I, both orientations, and all rational cylinder tests. It includes the actual tested measure identity at every admissible stage, as well as the full-error convergence and L2 bound.

   theorem sourceSampling_rational_event :
       ∀ᵐ θ ∂sourceAngleLaw, ∀ (I : Finset SourceCoordinate) (r : Bool)
         (T : SourceSamplingRationalTest),
         Tendsto (fun stage => sourceSamplingSquaredError stage r (fun i => decide (i ∈ I))
           (sourceSamplingRationalX T) (sourceSamplingRationalY T) θ) atTop (𝓝 0) ∧
         ∃ C : ℝ, ∀ stage,
           MemLp (sourceSamplingEmpiricalDensity stage r (fun i => decide (i ∈ I))
             (sourceSamplingRationalX T) (sourceSamplingRationalY T) θ) 2 sourceSamplingHaar ∧
           (∫ x, sourceSamplingEmpiricalDensity stage r (fun i => decide (i ∈ I))
             (sourceSamplingRationalX T) (sourceSamplingRationalY T) θ x ^ 2 ∂sourceSamplingHaar) ≤ C ∧
           (T.1 ⊆ sourceSamplingPrefix stage →
             ((sourceSamplingUntrimmed I stage θ).restrict
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingSquaredError, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingEmpiricalDensity, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingUntrimmed

9. theorem OAI.FiniteFactor.sourceSampling_both_marginals_event line 91

   Source documentation

   Both actual untested marginal densities are uniformly L2 bounded on one conull event, simultaneously for all finite I.

   theorem sourceSampling_both_marginals_event :
       ∀ᵐ θ ∂sourceAngleLaw, ∀ (I : Finset SourceCoordinate) (r : Bool),
         ∃ C : ℝ, ∀ stage, ∃ f : (SourceCoordinate → ℝ) → ℝ,
           (sourceSamplingUntrimmed I stage θ).map (sourceSamplingEndpoint r) =
             sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal (f x)) ∧
           MemLp f 2 sourceSamplingHaar ∧ (∫ x, f x^2 ∂sourceSamplingHaar) ≤ C := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingHaar