GoodSample.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous choice of small random quantities

The finite-transfer grid selection needs one sample for which both the wedge integral and terminal count are small, while retaining the conull compatibility conditions. The proof below uses the integral of the sum of the two normalized quantities, so its conclusion preserves any specified conull event.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_good_sample line 20

Source documentation

Two nonnegative integrable costs can simultaneously be kept below their thresholds when the sum of their normalized expectations is below one.

theorem exists_good_sample {X : Type*} [MeasurableSpace X] {μ : Measure X}
    [IsProbabilityMeasure μ] {f g : X → ℝ} {P : X → Prop} {A B : ℝ}
    (hA : 0 < A) (hB : 0 < B) (hf : Integrable f μ) (hg : Integrable g μ)
    (hf0 : ∀ᵐ x ∂μ, 0 ≤ f x) (hg0 : ∀ᵐ x ∂μ, 0 ≤ g x) (hP : ∀ᵐ x ∂μ, P x)
    (hmean : (∫ x, f x ∂μ) / A + (∫ x, g x ∂μ) / B < 1) :
    ∃ x, P x ∧ f x < A ∧ g x < B := by
…