StrongOneSample.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The stronger constant for the concrete one-sample rule

The introduction explicitly records the stronger 2⁻²⁹³ constant proved in accounting.tex. The root endpoint uses its announced 2⁻³¹⁰ constant. This supporting theorem exposes the stronger claim for the actual constructed rule, without changing the endpoint or imposing moments on individual loop values.

The rule and initial seed law below depend only on the known labeled matroid. The probability space, matching input laws, and full-seed-aware adversary are supplied afterwards. Feasibility is pointwise at every prefix and the reward estimate uses only integrability of the actual offline optimum.

theorem OAI.MatroidProphet.source_one_sample_feasible line 24
Source documentation
The actual simulated source rule is feasible before any laws are chosen.
```
theorem source_one_sample_feasible {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    Feasible M (sampleSimulation (completeHiddenRule M hE)) :=
…
```
Mentions: OAI.MatroidProphet.Feasible, OAI.MatroidProphet.sampleSimulation, OAI.MatroidProphet.completeHiddenRule

theorem OAI.MatroidProphet.source_one_sample_strong line 33

Source documentation

The source construction attains the stronger constant advertised after thm:main, even when the order sees the complete initial seed. This is a consequence for the concrete rule, not a premise asserting its performance.

theorem source_one_sample_strong {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (S V : Ω → Weights n) (R : Ω → Seed (mainSeedBits n))
    (hS : Measurable S) (hV : Measurable V) (hR : Measurable R)
    (hSN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ S ω e)
    (hVN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ V ω e)
    (hi : iIndepFun (pairedCoordinates S V) μ)
    (hlaw : ∀ e, μ.map (fun ω => S ω e) = μ.map (fun ω => V ω e))
    (hseed : IndepFun (fun ω => (S ω, V ω)) R μ)
    (hRlaw : μ.map R = sourceSeedLaw n)
    (hopt : Integrable (fun ω => optimum M (V ω)) μ)
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.pairedCoordinates, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.optimum