PhysicalParentDraw.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Parent random streams in a fixed child environment

Finite parent arrays contain independent uniform optimizer integers and actual shared-group draws. The projection laws are exact. Their use in the node bound needs only the individual marginals, so no independence between an online payoff and a group-failure indicator is asserted there.

abbrev OAI.EditApproximation.ParentGroupDraw line 18
abbrev OAI.EditApproximation.ParentRandomSpace line 21
def OAI.EditApproximation.parentDrawLaw line 24
instance OAI.EditApproximation.parentDrawLaw_probability line 30
def OAI.EditApproximation.parentOnlineDraw line 36
def OAI.EditApproximation.parentGroupDraw line 39
theorem OAI.EditApproximation.parentDrawLaw_online_mean line 42
theorem OAI.EditApproximation.parentDrawLaw_group_mean line 52

theorem OAI.EditApproximation.bool_indicator_integral line 63

Source documentation

A finite Boolean event has precisely its probability as expected indicator.

theorem bool_indicator_integral {Ω : Type*} [Fintype Ω]
    [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (μ : Measure Ω) (failure : Ω → Bool) :
    (∫ ω, (if failure ω then (1 : ℝ) else 0) ∂μ) = μ.real {ω | failure ω = true} := by
…

theorem OAI.EditApproximation.parentDrawLaw_group_failure_mean line 71

theorem OAI.EditApproximation.parentDrawLaw_firstCrossing_bound line 82

Source documentation

Integrating the deterministic first-crossing transfer needs only the exact online marginals and per-time group probabilities.

theorem parentDrawLaw_firstCrossing_bound (R O M K : ℕ) [NeZero R] [NeZero M] [NeZero O]
    [MeasurableSpace (Fin M)] [MeasurableSingletonClass (Fin M)]
    (count : Fin K → ℕ) (S C : ℕ)
    (regret : ParentRandomSpace R O M K count → ℕ → ℝ)
    (prefixPayoff : ℕ → Fin O → ℝ) (failure : ℕ → ParentGroupDraw M K count → Bool)
    (budget crossingCharge failureCharge q : ℝ) (hcharge : 0 ≤ failureCharge)
    (hpoint : ∀ ω, (∑ t ∈ range S, regret ω t) ≤
      (∑ t ∈ range C, prefixPayoff t (parentOnlineDraw ω t)) + crossingCharge +
        failureCharge * ∑ t ∈ range S, (if failure t (parentGroupDraw ω t) then (1 : ℝ) else 0))
    (hprefix : (∑ t ∈ range C, uniformMean (prefixPayoff t)) ≤ budget)
    (hfailure : ∀ t < S, (groupSharedDrawLaw (M := M) count).real {draw | failure t draw = true} ≤ q) :
…

Mentions: OAI.EditApproximation.ParentRandomSpace, OAI.EditApproximation.ParentGroupDraw, OAI.EditApproximation.parentOnlineDraw, OAI.EditApproximation.parentGroupDraw, OAI.EditApproximation.uniformMean, OAI.EditApproximation.groupSharedDrawLaw