BlockCapture.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Averaging and capture of nonnegative spectral mass

For any finite family of nonnegative masses and random detection events, if every low-degree support is detected with probability at least a, an upper bound on the average detected mass bounds the low-degree mass.

theorem OAI.Problem313.weighted_capture_sum_swap line 24

Source documentation

Interchange averaging over blocks and summing the mass of captured supports.

theorem weighted_capture_sum_swap
    (w : β → ℝ) (mass : ι → ℝ) (detect : β → ι → Prop)
    [DecidableRel detect] :
    (∑ b, w b * ∑ i, if detect b i then mass i else 0) =
      ∑ i, (∑ b, if detect b i then w b else 0) * mass i := by
…

theorem OAI.Problem313.capture_mass_mul_le line 38

Source documentation

A pointwise detection lower bound controls the mass on any chosen finite set.

theorem capture_mass_mul_le
    (low : Finset ι) (mass detection : ι → ℝ) (a : ℝ)
    (hmass : ∀ i, 0 ≤ mass i) (hdet : ∀ i, 0 ≤ detection i)
    (hlow : ∀ i ∈ low, a ≤ detection i) :
    a * ∑ i ∈ low, mass i ≤ ∑ i, detection i * mass i := by
…

theorem OAI.Problem313.averaged_capture_mass_mul_le line 52

Source documentation

The same capture inequality stated directly with finite block averaging.

theorem averaged_capture_mass_mul_le
    (low : Finset ι) (w : β → ℝ) (mass : ι → ℝ)
    (detect : β → ι → Prop) [DecidableRel detect] (a : ℝ)
    (hw : ∀ b, 0 ≤ w b) (hmass : ∀ i, 0 ≤ mass i)
    (hlow : ∀ i ∈ low, a ≤ ∑ b, if detect b i then w b else 0) :
    a * ∑ i ∈ low, mass i ≤
      ∑ b, w b * ∑ i, if detect b i then mass i else 0 := by
…

theorem OAI.Problem313.block_capture_mass_le line 71

Source documentation

Cancel the random-block detection factor. The factor 4 is exactly the ratio between the edge-touch upper bound 2*m/n and detection m/(2*n).

theorem block_capture_mass_le
    (low : Finset ι) (w : β → ℝ) (mass : ι → ℝ)
    (detect : β → ι → Prop) [DecidableRel detect]
    (m n Q : ℝ) (hm : 0 < m) (hn : 0 < n)
    (hw : ∀ b, 0 ≤ w b) (hmass : ∀ i, 0 ≤ mass i)
    (hlow : ∀ i ∈ low, m / (2 * n) ≤ ∑ b, if detect b i then w b else 0)
    (haverage : (∑ b, w b * ∑ i, if detect b i then mass i else 0) ≤
      (2 * m / n) * Q) :
    (∑ i ∈ low, mass i) ≤ 4 * Q := by
…