BanditRLProof.LowerBounds.CommonDensityOverlap

Square roots of nonnegative integrable functions belong to L2.

theorem memLp_sqrt_of_integrable_nonneg {α : Type*} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} (hf : Integrable f μ) (hpos : ∀ x, 0 ≤ f x) : MemLp (fun x => Real.sqrt (f x)) 2 μ

Cauchy--Schwarz for the square-root affinity integrand.

theorem integral_sqrt_mul_sq_le {α : Type*} [MeasurableSpace α] {μ : Measure α} {p q : α → ℝ} (hp : Integrable p μ) (hq : Integrable q μ) (hp0 : ∀ x, 0 ≤ p x) (hq0 : ∀ x, 0 ≤ q x) : (∫ x, Real.sqrt (p x * q x) ∂μ) ^ 2 ≤ (∫ x, p x ∂μ) * ∫ x, q x ∂μ

Integral of the pointwise minimum of common RN densities.

def commonDensityOverlap {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) : ℝ

Hellinger affinity of two densities relative to a common measure.

def commonDensityAffinity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_commonDensityAffinity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : Integrable (fun x => Real.sqrt ((P.rnDeriv μ x).toReal * (Q.rnDeriv μ x).toReal)) μ

Eq. (14.9), including integrable densities with zeros.

theorem half_commonDensityAffinity_sq_le_overlap {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : (1 / 2 : ℝ) * commonDensityAffinity P Q μ ^ 2 ≤ commonDensityOverlap P Q μ

The event selecting the smaller source density.

def commonDensityComparisonEvent {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) : Set α

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurableSet_commonDensityComparisonEvent {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) : MeasurableSet (commonDensityComparisonEvent P Q μ)

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_min_commonDensity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : Integrable (fun x => min (P.rnDeriv μ x).toReal (Q.rnDeriv μ x).toReal) μ

No declaration docstring is present; use the chapter context and exact statement below.

theorem commonDensityOverlap_nonneg {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) : 0 ≤ commonDensityOverlap P Q μ

The likelihood comparison event attains the density-overlap testing error.

theorem commonDensityOverlap_eq_testingError {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : commonDensityOverlap P Q μ = P.real (commonDensityComparisonEvent P Q μ) + Q.real (commonDensityComparisonEvent P Q μ)ᶜ

The overlap is no larger than the testing error of any measurable event.

theorem commonDensityOverlap_le_testingError {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) {A : Set α} (hA : MeasurableSet A) : commonDensityOverlap P Q μ ≤ P.real A + Q.real Aᶜ

Eq. (14.8): the measure overlap is bounded below by the BH exponential scale.

theorem bretagnolleHuberScale_le_commonDensityOverlap {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : bretagnolleHuberScale (relativeEntropy P Q) ≤ commonDensityOverlap P Q μ