OAI/Analysis/FiniteFactor/BiasedPairs/Measures.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceBiasedSample line 13
2. abbrev OAI.FiniteFactor.sourceBiasedLaw line 14
3. def OAI.FiniteFactor.sourceBiasedEndpoint line 17
4. theorem OAI.FiniteFactor.sourceBiasedEndpoint_measurable line 20
5. def OAI.FiniteFactor.sourceBiasedPair line 24

   Source documentation

   The mixed pair has the original x endpoint and selects x or y coordinatewise.

   def sourceBiasedPair (r : SourceCoordinate → Bool) (ω : SourceBiasedSample) : SourceSamplingPair :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBiasedSample, OAI.FiniteFactor.SourceSamplingPair

6. theorem OAI.FiniteFactor.sourceBiasedPair_measurable line 27
7. def OAI.FiniteFactor.sourceBiasedRealMeasure line 30
8. instance OAI.FiniteFactor.sourceBiasedRealMeasure_probability line 33
9. def OAI.FiniteFactor.sourceBiasedTorusMeasure line 37
10. theorem OAI.FiniteFactor.sourceBiasedRealMeasure_marginal line 40
11. theorem OAI.FiniteFactor.sourceBiasedEndpoint_density line 48

    Source documentation

    A nonnegative measurable version of each actual marginal density.

    theorem sourceBiasedEndpoint_density (j : ℕ) (r : SourceCoordinate → Bool) :
        ∃ g : (SourceCoordinate → ℝ) → ℝ, Measurable g ∧ (∀ x, 0 ≤ g x) ∧
          MemLp g 2 sourceSamplingHaar ∧
          (sourceBiasedLaw j).map (sourceBiasedEndpoint r) =
            sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal (g x)) ∧
          (∫ x, g x^2 ∂sourceSamplingHaar) ≤ Real.exp (20*(2*(∑' s,sourceKappa s^2)+1)) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceKappa

12. theorem OAI.FiniteFactor.sourceBiasedTorusMeasure_density line 65

    Source documentation

    Both mixed torus marginals have the same actual uniform L2 bound.

    theorem sourceBiasedTorusMeasure_density (j : ℕ) (r : SourceCoordinate → Bool) (b : Bool) :
        ∃ g : SourceTorus → ℝ, Measurable g ∧ (∀ z, 0 ≤ g z) ∧
          MemLp g 2 sourceTorusHaar ∧
          (sourceBiasedTorusMeasure j r : Measure SourceSamplingTorus).map (sourceTorusEndpoint b) =
            sourceTorusHaar.withDensity (fun z => ENNReal.ofReal (g z)) ∧
          (∫ z, g z^2 ∂sourceTorusHaar) ≤ Real.exp (20*(2*(∑' s,sourceKappa s^2)+1)) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint, OAI.FiniteFactor.sourceKappa

13. theorem OAI.FiniteFactor.sourceBiasedTorusMeasure_marginal_ac line 87

    Source documentation

    Every endpoint of every mixed-prefix or full biased law belongs to any prescribed Haar-conull Borel set.

    theorem sourceBiasedTorusMeasure_marginal_ac (j : ℕ) (r : SourceCoordinate → Bool) (b : Bool) :
        (sourceBiasedTorusMeasure j r : Measure SourceSamplingTorus).map (sourceTorusEndpoint b) ≪ sourceTorusHaar := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint, OAI.FiniteFactor.sourceTorusHaar