Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersCombine.combine_eq_cases
Project documentation
Definition 4.11.2 Combine(d*, r, (f_0, d_0), …, (f_{m-1}, d_{m-1}))(x) := if (r * φ(x)) = 1 then sum_{i < m} r_i * f_i(x) * (dstar - degree + 1) else sum_{i < m} r_i * f_i(x) * (1 - r * φ(x)^(dstar - degree + 1)) / (1 - r * φ(x))
Source project: ArkLib
Person-level attribution pending.
Combine.combine_theorem
Plain-language statement
Lemma 4.13 Let dstar be the target degree, f₁,...,f_{m-1} : ι → F, 0 < degs₁,...,degs_{m-1} < dstar be degrees and δ ∈ (0, min{(1-BStar(ρ)), (1-ρ-1/|ι|)}) be a distance parameter, then Pr_{r ← F} [δᵣ(Combine(dstar,r,(f₁,degs₁),...,(fₘ,degsₘ)))] > err' (dstar, ρ, δ, m * (dstar + 1) - ∑ i degsᵢ)
Source project: ArkLib
Person-level attribution pending.