FiniteWeightLawTheorems.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Finite conditional-kernel bridge for the secretary transport. The algebraic fiber identity is a hypothesis of these reusable lemmas, not a substitute for proving that identity for the manuscript's actual source-seed law.

theorem OAI.MatroidProphet.FiniteLaw.weightPMF_apply line 18
instance OAI.MatroidProphet.FiniteLaw.weightMeasure_probability line 22
theorem OAI.MatroidProphet.FiniteLaw.weightMeasure_singleton line 28
theorem OAI.MatroidProphet.FiniteLaw.integral_weightMeasure line 33
theorem OAI.MatroidProphet.FiniteLaw.sum_real_singleton line 39
theorem OAI.MatroidProphet.FiniteLaw.weightMeasure_real_singleton line 46
Source documentation
No finite-law assumption is added: every probability measure on a finite discrete space is exactly the measure of its real singleton weights.
```
theorem weightMeasure_real_singleton [MeasurableSpace α] [MeasurableSingletonClass α]
    (μ : Measure α) [IsProbabilityMeasure μ] :
    weightMeasure (fun a => μ.real {a}) (fun _ => measureReal_nonneg)
      (sum_real_singleton μ) = μ := by
…
```
Mentions: OAI.MatroidProphet.FiniteLaw.weightMeasure, OAI.MatroidProphet.FiniteLaw.sum_real_singleton
theorem OAI.MatroidProphet.FiniteLaw.map_real_singleton line 56
theorem OAI.MatroidProphet.FiniteLaw.kernelJointPMF_apply line 70
instance OAI.MatroidProphet.FiniteLaw.kernelJointMeasure_probability line 77
theorem OAI.MatroidProphet.FiniteLaw.integral_kernelJointMeasure line 85
theorem OAI.MatroidProphet.FiniteLaw.kernelJointPMF_eq_map line 100
theorem OAI.MatroidProphet.FiniteLaw.kernelJointMeasure_eq_map line 122

theorem OAI.MatroidProphet.FiniteLaw.integral_reconstruction line 138

Source documentation

The joint law transports every statistic of the observation and full seed, not merely statistics of the sacrificed mask.

theorem integral_reconstruction
    [MeasurableSpace α] [MeasurableSingletonClass α]
    [MeasurableSpace β] [MeasurableSingletonClass β]
    (p : α → ℝ) (hp : ∀ a, 0 ≤ p a) (hp1 : ∑ a, p a = 1)
    (obs : α → β) (m : β → ℝ) (k : β → α → ℝ)
    (hm : ∀ b, 0 ≤ m b) (hm1 : ∑ b, m b = 1)
    (hk : ∀ b a, 0 ≤ k b a) (hk1 : ∀ b, ∑ a, k b a = 1)
    (hjoint : ∀ b a, m b * k b a = if obs a = b then p a else 0)
    (f : β × α → ℝ) :
    (∫ b, ∫ a, f (b, a) ∂weightMeasure (k b) (hk b) (hk1 b)
        ∂weightMeasure m hm hm1) =
      ∫ a, f (obs a, a) ∂weightMeasure p hp hp1 := by
…

Mentions: OAI.MatroidProphet.FiniteLaw.weightMeasure

theorem OAI.MatroidProphet.FiniteLaw.observation_eq_of_joint_support line 157

Source documentation

Every positive-mass reconstructed joint outcome has exactly its advertised observation. Zero-mass fibers are not silently ruled out.

theorem observation_eq_of_joint_support
    (p : α → ℝ) (obs : α → β) (m : β → ℝ) (k : β → α → ℝ)
    (hm : ∀ b, 0 ≤ m b) (hm1 : ∑ b, m b = 1)
    (hk : ∀ b a, 0 ≤ k b a) (hk1 : ∀ b, ∑ a, k b a = 1)
    (hjoint : ∀ b a, m b * k b a = if obs a = b then p a else 0)
    (b : β) (a : α)
    (ha : (b, a) ∈ (kernelJointPMF m k hm hm1 hk hk1).support) : obs a = b := by
…

Mentions: OAI.MatroidProphet.FiniteLaw.kernelJointPMF