OAI/Combinatorics/SharpThreshold/BlockAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.BlockAverage.weighted_incidence_sum line 14

   Source documentation

   Exchange the average over blocks with a sum over objects detected by a block.

   theorem weighted_incidence_sum
       {α : Type u} {β : Type v} [Fintype α] [Fintype β]
       (μ : β → ℝ) (w : α → ℝ) (P : β → α → Prop)
       [DecidableRel P] :
       (∑ b, μ b * ∑ s, if P b s then w s else 0) =
         ∑ s, (∑ b, if P b s then μ b else 0) * w s := by
   …

2. theorem OAI.Problem313.BlockAverage.incidence_sum_nonneg line 30

   Source documentation

   Nonnegative block weights give nonnegative incidence probabilities.

   theorem incidence_sum_nonneg
       {β : Type v} [Fintype β] (μ : β → ℝ) (P : β → Prop)
       [DecidablePred P] (hμ : ∀ b, 0 ≤ μ b) :
       0 ≤ ∑ b, if P b then μ b else 0 := by
   …

3. theorem OAI.Problem313.BlockAverage.capture_lower_bound line 42

   Source documentation

   A collection of nonnegative masses detected with probability at least c contributes at least c times its total mass to the average detected mass.

   theorem capture_lower_bound
       {α : Type u} {β : Type v} [Fintype α] [Fintype β]
       (μ : β → ℝ) (w : α → ℝ) (P : β → α → Prop)
       [DecidableRel P] (low : Finset α) (c : ℝ)
       (hμ : ∀ b, 0 ≤ μ b) (hw : ∀ s, 0 ≤ w s)
       (hcapture : ∀ s ∈ low, c ≤ ∑ b, if P b s then μ b else 0) :
       c * ∑ s ∈ low, w s ≤ ∑ b, μ b * ∑ s, if P b s then w s else 0 := by
   …

4. theorem OAI.Problem313.BlockAverage.block_upper_bound line 63

   Source documentation

   Pointwise block bounds average to a global bound using the incidence probability of each coordinate. No normalization assumption is required.

   theorem block_upper_bound
       {α : Type u} {β : Type v} {ι : Type w} [Fintype α] [Fintype β] [Fintype ι]
       (μ : β → ℝ) (w : α → ℝ) (I : ι → ℝ)
       (P : β → α → Prop) (E : β → ι → Prop)
       [DecidableRel P] [DecidableRel E] (a d : ℝ)
       (hμ : ∀ b, 0 ≤ μ b) (hI : ∀ i, 0 ≤ I i) (ha : 0 ≤ a)
       (hblock : ∀ b, (∑ s, if P b s then w s else 0) ≤
         a * ∑ i, if E b i then I i else 0)
       (hincidence : ∀ i, (∑ b, if E b i then μ b else 0) ≤ d) :
       (∑ b, μ b * ∑ s, if P b s then w s else 0) ≤ a * d * ∑ i, I i := by
   …

5. theorem OAI.Problem313.BlockAverage.captured_mass_le line 95

   Source documentation

   The algebraic block-capture argument, with arbitrary capture and incidence constants. It separates all finite averaging from the Fourier and graph input.

   theorem captured_mass_le
       {α : Type u} {β : Type v} {ι : Type w} [Fintype α] [Fintype β] [Fintype ι]
       (μ : β → ℝ) (w : α → ℝ) (I : ι → ℝ)
       (P : β → α → Prop) (E : β → ι → Prop)
       [DecidableRel P] [DecidableRel E] (low : Finset α) (a c d : ℝ)
       (hμ : ∀ b, 0 ≤ μ b) (hw : ∀ s, 0 ≤ w s)
       (hI : ∀ i, 0 ≤ I i) (ha : 0 ≤ a) (hc : 0 < c)
       (hcapture : ∀ s ∈ low, c ≤ ∑ b, if P b s then μ b else 0)
       (hblock : ∀ b, (∑ s, if P b s then w s else 0) ≤
         a * ∑ i, if E b i then I i else 0)
       (hincidence : ∀ i, (∑ b, if E b i then μ b else 0) ≤ d) :
       (∑ s ∈ low, w s) ≤ (a * d / c) * ∑ i, I i := by
   …

6. theorem OAI.Problem313.BlockAverage.captured_mass_le_four line 117

   Source documentation

   The factor-four consequence used for uniform vertex blocks: capture at least m/(2*n) and edge incidence at most 2*m/n.

   theorem captured_mass_le_four
       {α : Type u} {β : Type v} {ι : Type w} [Fintype α] [Fintype β] [Fintype ι]
       (μ : β → ℝ) (w : α → ℝ) (I : ι → ℝ)
       (P : β → α → Prop) (E : β → ι → Prop)
       [DecidableRel P] [DecidableRel E] (low : Finset α) (a c : ℝ)
       (hμ : ∀ b, 0 ≤ μ b) (hw : ∀ s, 0 ≤ w s)
       (hI : ∀ i, 0 ≤ I i) (ha : 0 ≤ a) (hc : 0 < c)
       (hcapture : ∀ s ∈ low, c ≤ ∑ b, if P b s then μ b else 0)
       (hblock : ∀ b, (∑ s, if P b s then w s else 0) ≤
         a * ∑ i, if E b i then I i else 0)
       (hincidence : ∀ i, (∑ b, if E b i then μ b else 0) ≤ 4 * c) :
       (∑ s ∈ low, w s) ≤ 4 * a * ∑ i, I i := by
   …

7. theorem OAI.Problem313.BlockAverage.uniform_incidence_sum line 137

   Source documentation

   Uniform finite sampling agrees with the normalized cardinality used by the vertex-block counting lemmas. This also holds for an empty sampling family.

   theorem uniform_incidence_sum
       {β : Type v} [DecidableEq β] (Ω : Finset β) (P : β → Prop)
       [DecidablePred P] :
       (∑ b : Ω, if P b.val then (1 : ℝ) / Ω.card else 0) =
         ((Ω.filter P).card : ℝ) / Ω.card := by
   …

8. theorem OAI.Problem313.BlockAverage.captured_mass_le_four_uniform line 149

   Source documentation

   Uniform-block version of the factor-four capture argument, stated entirely with cardinal-ratio probabilities to match the combinatorial counting API.

   theorem captured_mass_le_four_uniform
       {α : Type u} {β : Type v} {ι : Type w} [Fintype α] [DecidableEq β] [Fintype ι]
       (Ω : Finset β) (w : α → ℝ) (I : ι → ℝ)
       (P : β → α → Prop) (E : β → ι → Prop)
       [DecidableRel P] [DecidableRel E] (low : Finset α) (a c : ℝ)
       (hw : ∀ s, 0 ≤ w s) (hI : ∀ i, 0 ≤ I i)
       (ha : 0 ≤ a) (hc : 0 < c)
       (hcapture : ∀ s ∈ low, c ≤
         ((Ω.filter (fun b => P b s)).card : ℝ) / Ω.card)
       (hblock : ∀ b ∈ Ω, (∑ s, if P b s then w s else 0) ≤
         a * ∑ i, if E b i then I i else 0)
       (hincidence : ∀ i,
   …