RoundingExpectation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The upper expectation bound for rounding

The score sums over nonempty subsets of the original ground set. Its moments come from the actual coordinate product law. Nonemptiness saves a factor of one fifth in the fractional-cover cost.

def OAI.TalagrandThreshold.productScore line 26
Source documentation
The nonnegative subset-product score used by the rounding argument.
```
def productScore (g : Finset α → ℝ) (Y : α → ℝ) : ℝ :=
…
```
theorem OAI.TalagrandThreshold.productScore_nonneg line 29

theorem OAI.TalagrandThreshold.expectation_productScore line 37

Source documentation

Independence of the coordinates gives the full subset-product expectation.

theorem expectation_productScore (ν : FiniteLaw Ω) (g : Finset α → ℝ) (Y : Ω → ℝ) :
    (FiniteLaw.pi (fun _ : α => ν)).expectation
        (fun ω => productScore g (fun x => Y (ω x))) =
      ∑ S ∈ (Finset.univ.erase ∅ : Finset (Finset α)),
        g S * (ν.expectation Y) ^ S.card := by
…

Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.productScore

theorem OAI.TalagrandThreshold.one_fifth_pow_le line 56
Source documentation
A nonempty product gains at least one factor of one fifth.
```
theorem one_fifth_pow_le {r : ℝ} (hr : 0 ≤ r) {k : ℕ} (hk : 0 < k) :
    (r / 5) ^ k ≤ (1 / 5) * r ^ k := by
…
```

theorem OAI.TalagrandThreshold.expectation_productScore_le line 68

Source documentation

The product score costs at most one fifth of the fractional-cover cost.

theorem expectation_productScore_le (ν : FiniteLaw Ω) (g : Finset α → ℝ)
    (Y : Ω → ℝ) {r : ℝ} (hg : ∀ S, 0 ≤ g S) (hY : ∀ ω, 0 ≤ Y ω)
    (hr : 0 ≤ r) (hmean : ν.expectation Y ≤ r / 5) :
    (FiniteLaw.pi (fun _ : α => ν)).expectation
        (fun ω => productScore g (fun x => Y (ω x))) ≤
      (1 / 5) * fracCost r g := by
…

Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.productScore, OAI.TalagrandThreshold.fracCost

theorem OAI.TalagrandThreshold.expectation_productScore_le_tenth line 102

Source documentation

The budget one half gives the upper bound one tenth for the same score.

theorem expectation_productScore_le_tenth (ν : FiniteLaw Ω) (g : Finset α → ℝ)
    (Y : Ω → ℝ) {r : ℝ} (hg : ∀ S, 0 ≤ g S) (hY : ∀ ω, 0 ≤ Y ω)
    (hr : 0 ≤ r) (hmean : ν.expectation Y ≤ r / 5) (hcost : fracCost r g ≤ 1 / 2) :
    (FiniteLaw.pi (fun _ : α => ν)).expectation
        (fun ω => productScore g (fun x => Y (ω x))) ≤ 1 / 10 := by
…

Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.fracCost, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.productScore