TestedSelfMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sampling_square_integrable line 11

Source documentation

A bounded measurable real function has an integrable square on a finite measure.

theorem sampling_square_integrable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsFiniteMeasure μ] (f : Ω → ℝ) (C : ℝ) (hm : Measurable f)
    (hb : ∀ x, 0 ≤ f x ∧ f x ≤ C) : Integrable (fun x => f x ^ 2) μ := by
…

theorem OAI.FiniteFactor.samplingWeight_square_integrable line 20
Source documentation
Squared weights are integrable jointly, permitting the source's Fubini step.
```
theorem samplingWeight_square_integrable (b : Bool) (h α : ℝ) (hh : 0 < h) (hα : 0 < α) :
    Integrable (fun p : ℝ × ℝ => samplingWeight b h α p.1 p.2 ^ 2)
      (unitIntervalMeasure.prod unitIntervalMeasure) :=
…
```
Mentions: OAI.FiniteFactor.samplingWeight, OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.samplingSecondWeight_square_integral line 28
Source documentation
Haar translation preserves the untested self-pair moment in the second orientation, with the source's order of both integrations.
```
theorem samplingSecondWeight_square_integral (h α : ℝ) (hh : 0 < h) (hh1 : h < 1)
    (hα : 0 < α) (hα1 : α ≤ 1/2) :
    (∫ s, ∫ t, samplingSecondWeight h α s t ^ 2
      ∂unitIntervalMeasure ∂unitIntervalMeasure) = (2/h)*Real.log (1/(2*α)) := by
…
```
Mentions: OAI.FiniteFactor.samplingSecondWeight, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.samplingTestedFirstWeight_square_integral line 54

Source documentation

Tests decrease the diagonal self-pair moment in the first orientation.

theorem samplingTestedFirstWeight_square_integral (h α : ℝ) (E G : Set ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hα1 : α ≤ 1/2)
    (hE : MeasurableSet E) (hG : MeasurableSet G) :
    (∫ s, ∫ t, samplingTestedFirstWeight false h α E G s t ^ 2
      ∂unitIntervalMeasure ∂unitIntervalMeasure) ≤ (2/h)*Real.log (1/(2*α)) := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.samplingTestedSecondWeight_square_integral line 74

Source documentation

Tests decrease the diagonal self-pair moment in the second orientation.

theorem samplingTestedSecondWeight_square_integral (h α : ℝ) (E G : Set ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hα1 : α ≤ 1/2)
    (hE : MeasurableSet E) (hG : MeasurableSet G) :
    (∫ s, ∫ t, samplingTestedSecondWeight h α E G s t ^ 2
      ∂unitIntervalMeasure ∂unitIntervalMeasure) ≤ (2/h)*Real.log (1/(2*α)) := by
…

Mentions: OAI.FiniteFactor.samplingTestedSecondWeight, OAI.FiniteFactor.unitIntervalMeasure