OAI/Analysis/FiniteFactor/OrbitSampling/PhaseSelfMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_phase_square_bound line 12

   Source documentation

   Marginal phase domination controls the joint self-pair integral. This is the source's one-phase step before taking coordinate products.

   theorem sampling_phase_square_bound {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (hX : Measurable X)
       (hdom : μ.map X ≤ (2 : ℝ≥0∞) • unitIntervalMeasure)
       (u : ℝ → ℝ → ℝ) (C : ℝ) (hu : Measurable (fun p : ℝ × ℝ => u p.1 p.2))
       (hb : ∀ s t, 0 ≤ u s t ∧ u s t ≤ C) :
       (∫ s, ∫ ω, u s (X ω)^2 ∂μ ∂unitIntervalMeasure) ≤
         2*(∫ s, ∫ t, u s t^2 ∂unitIntervalMeasure ∂unitIntervalMeasure) := by
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure

2. theorem OAI.FiniteFactor.sourceSampling_phase_self_moment line 41

   Source documentation

   Actual angle expectation of the tested self-pair, at every admissible selected power, for all source orientations and coordinate types.

   theorem sourceSampling_phase_self_moment (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
       (i : SourceCoordinate) (hi : i.1 ≤ stage) (n : ℤ) (hn : n ∈ sourceSamplingPowers stage)
       (r b : Bool) (E G : Set ℝ) (hE : MeasurableSet E) (hG : MeasurableSet G) :
       (∫ s, ∫ θ, samplingOrientedWeight r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
         E G s (Int.fract ((n : ℝ)*θ i)) ^ 2 ∂sourceAngleLaw ∂unitIntervalMeasure) ≤
         2+8*(sourceBlockSize stage : ℝ)^(3/5 : ℝ)*Real.log (sourceBlockSize stage : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.unitIntervalMeasure