OAI/Analysis/FiniteFactor/OrbitSampling/Weights.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingWidth line 11
2. def OAI.FiniteFactor.sourceSamplingCutoff line 12
3. def OAI.FiniteFactor.sourceSamplingPrefix line 13
4. theorem OAI.FiniteFactor.sourceSampling_parameters line 16
5. theorem OAI.FiniteFactor.sourceSampling_weight_bound line 22
6. def OAI.FiniteFactor.sourceSamplingWeight line 40
7. theorem OAI.FiniteFactor.sourceSamplingWeight_measurable line 46
8. theorem OAI.FiniteFactor.sourceSamplingWeight_bounds line 54
9. theorem OAI.FiniteFactor.sourceSamplingWeight_memLp line 69

   Source documentation

   Each actual finite-stage weight has an L2 density. This bound is for one stage; it does not assert the later uniform-in-stage sampling bound.

   theorem sourceSamplingWeight_memLp (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) (n : ℤ) :
       MemLp (sourceSamplingWeight I s θ n) 2
         (Measure.infinitePi (fun _ : SourceCoordinate => unitIntervalMeasure)) := by
   …

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

10. theorem OAI.FiniteFactor.sourceSamplingWeight_prefix line 80

    Source documentation

    The actual density depends only on the prefix, before tail trimming.

    theorem sourceSamplingWeight_prefix (I : Finset SourceCoordinate) (s : ℕ)
        (θ : SourceCoordinate → ℝ) (n : ℤ) (x y : SourceCoordinate → ℝ)
        (hxy : ∀ i ∈ sourceSamplingPrefix s, x i = y i) :
        sourceSamplingWeight I s θ n x = sourceSamplingWeight I s θ n y := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingWeight

11. theorem OAI.FiniteFactor.sourceSamplingWeight_orders_prefix line 89

    Source documentation

    Every nonzero summand orders all prefix coordinates under the actual rotation.

    theorem sourceSamplingWeight_orders_prefix (I : Finset SourceCoordinate) (s : ℕ)
        (θ : SourceCoordinate → ℝ) (n : ℤ) (x : SourceCoordinate → ℝ)
        (hx : ∀ i, x i ∈ Set.Ico (0 : ℝ) 1) (hw : sourceSamplingWeight I s θ n x ≠ 0) :
        ∀ i ∈ sourceSamplingPrefix s, x i < coordinateRotate θ n x i := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingWeight, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.coordinateRotate