FreshCoordinateCost.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A first request can depend on earlier answers, but cannot depend on its own unexposed coordinate. Finite product independence then preserves that coordinate's unconditional expected cost.

theorem OAI.EditApproximation.FiniteQuery.mem_keys_iff_of_agree_off line 25

Source documentation

Changing an oracle only at key does not change whether key is requested. The two executions agree up to its first request.

theorem mem_keys_iff_of_agree_off {ι : Type*} [DecidableEq ι]
    (left right : ι → ℚ) (key : ι)
    (hagrees : ∀ other, other ≠ key → left other = right other)
    (query : FiniteQuery ι) : key ∈ query.keys left ↔ key ∈ query.keys right := by
…

Mentions: OAI.EditApproximation.FiniteQuery

theorem OAI.EditApproximation.sum_distinct_requests_le line 41
theorem OAI.EditApproximation.sum_selected_nat_weights_le line 58

theorem OAI.EditApproximation.fresh_coordinate_independent line 78

Source documentation

Selection stable under replacing its own coordinate is independent of that coordinate. No accuracy event is used.

theorem fresh_coordinate_independent (i : ι) (selected : (∀ j, X j) → Prop)
    (hstable : ∀ left right : ∀ j, X j,
      (∀ j, j ≠ i → left j = right j) → (selected left ↔ selected right))
    (cost : X i → ℝ) :
    IndepFun (fun draw => selectionIndicator (selected draw))
      (fun draw => cost (draw i)) (Measure.pi μ) := by
…

Mentions: OAI.EditApproximation.selectionIndicator

theorem OAI.EditApproximation.fresh_coordinate_expected_cost line 105

theorem OAI.EditApproximation.fresh_coordinates_expected_sum_le line 119

Source documentation

Summing the first-request charges costs at most the expected selected width budget times the common per-width cost.

theorem fresh_coordinates_expected_sum_le
    (selected : ι → (∀ j, X j) → Prop)
    (hstable : ∀ i left right,
      (∀ j, j ≠ i → left j = right j) → (selected i left ↔ selected i right))
    (cost : (i : ι) → X i → ℝ) (width : ι → ℝ) (overhead budget : ℝ)
    (hoverhead : 0 ≤ overhead)
    (hcost : ∀ i, (∫ value, cost i value ∂μ i) ≤ width i * overhead)
    (hbudget : ∀ draw, ∑ i, (selectionIndicator (selected i draw)) * width i ≤ budget) :
    (∫ draw, ∑ i, (selectionIndicator (selected i draw)) * cost i (draw i) ∂Measure.pi μ) ≤
      budget * overhead := by
…

Mentions: OAI.EditApproximation.selectionIndicator

theorem OAI.EditApproximation.finiteQuery_fresh_expected_cost_le line 150

Source documentation

Concrete specialization to a finite adaptive read program. A key is charged once even if later continuation code requests it repeatedly.

theorem finiteQuery_fresh_expected_cost_le (query : FiniteQuery ι)
    (answer : (i : ι) → X i → ℚ) (cost : (i : ι) → X i → ℝ)
    (width : ι → ℝ) (overhead budget : ℝ) (hoverhead : 0 ≤ overhead)
    (hcost : ∀ i, (∫ value, cost i value ∂μ i) ≤ width i * overhead)
    (hbudget : ∀ draw : ∀ j, X j,
      ∑ i, (selectionIndicator (i ∈ query.keys (fun j => answer j (draw j)))) * width i ≤ budget) :
    (∫ draw, ∑ i,
      (selectionIndicator (i ∈ query.keys (fun j => answer j (draw j)))) * cost i (draw i)
        ∂Measure.pi μ) ≤ budget * overhead := by
…

Mentions: OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.selectionIndicator