FiniteResampling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate-refresh identities for finite product probability laws.

theorem OAI.EditApproximation.finite_pi_update_map line 20

Source documentation

Refreshing one coordinate with its own independent law preserves the complete finite product law.

theorem finite_pi_update_map (i : ι) :
    ((Measure.pi μ).prod (μ i)).map
      (fun pair : (∀ j, X j) × X i => Function.update pair.1 i pair.2) = Measure.pi μ := by
…

theorem OAI.EditApproximation.finite_pi_integral_update line 55

Source documentation

Integrating a fresh coordinate, then the complete original array, is exactly integration in the original product law.

theorem finite_pi_integral_update (i : ι) (payoff : (∀ j, X j) → ℝ) :
    (∫ original, ∫ fresh, payoff (Function.update original i fresh) ∂μ i ∂Measure.pi μ) =
      ∫ original, payoff original ∂Measure.pi μ := by
…

theorem OAI.EditApproximation.finite_pi_integral_update_pair line 70

Source documentation

Two independent refreshed coordinates provide the local parent law. The original arrays may still contain their previous values at those keys.

theorem finite_pi_integral_update_pair (i j : ι) (payoff : (∀ k, X k) → ℝ) :
    (∫ original, ∫ fresh : X i × X j,
      payoff (Function.update (Function.update original i fresh.1) j fresh.2)
        ∂(μ i).prod (μ j) ∂Measure.pi μ) =
      ∫ original, payoff original ∂Measure.pi μ := by
…

theorem OAI.EditApproximation.finite_pi_integral_bound_of_update_pair line 86

Source documentation

A pointwise bound after exact coordinate refresh integrates to the unconditional bound in the original global product.

theorem finite_pi_integral_bound_of_update_pair (i j : ι)
    (payoff budget : (∀ k, X k) → ℝ)
    (hbound : ∀ original, (∫ fresh : X i × X j,
      payoff (Function.update (Function.update original i fresh.1) j fresh.2) ∂(μ i).prod (μ j)) ≤
        budget original) :
    (∫ original, payoff original ∂Measure.pi μ) ≤ ∫ original, budget original ∂Measure.pi μ := by
…