QSearch: amplitude amplification with unknown amplitude, the expected cost (BHMT Theorem 3)

Category: 1-Mathlib (CSD-free).

BHMT's QSearch runs amplitude amplification in stages l = 0, 1, 2, … with the guesses M_l = ⌈(6/5)^l⌉: at each stage it measures a fresh copy of ψ directly, and failing that draws a round count j uniformly below M_l, amplifies a fresh copy j rounds and measures. Their Theorem 3: the expected number of applications of A and A⁻¹ before a good element is found is O(1/√a), with a = goodProb G ψ the unknown success probability.

• The stage law. stageProbAt G ψ j = a + (1 − a) · goodProb (Q^j ψ) is the success probability of a stage at round count j (the direct measurement, then the amplified one on a fresh copy); stageProb G ψ M averages it over j < M. Once M · sin 2θ ≥ 1 the average is at least 1/4 (quarter_le_stageProb, from the engine qsearch_average), and it is always at least a (le_stageProb).
• The run as a random process (QSearchRun): on a probability space, stage l draws its round count J l and records its success W l; the stages are independent (iIndepFun), J l is uniform below M_l, and given J l = j the stage succeeds with the Born probability stageProbAt G ψ j. The applications charged to a reached stage are 2 + 2 J l — the direct run, the fresh preparation, and two per round — and cost sums them over the reached stages.
• The bookkeeping. Stage l is reached with probability ∏_{k<l} (1 − p_k) (meas_reach, from independence), a reached stage costs M_l + 1 in expectation (lintegral_stageCost, independence of the fresh draw from the past), so the expected cost is ∑_l (M_l + 1) ∏_{k<l} (1 − p_k) (lintegral_cost). Past the critical stage every p_k ≥ 1/4, so the reach probabilities decay like (3/4)^{l − l₀} (meas_reach_le), and the series is bounded by the explicit geometric weights qsearchWeight (qsearch_partial_sum_le: 45 · (6/5)^{l₀}).
• ★★ BHMT Theorem 3 (qsearch_expected_cost): for 0 < a < 1, the expected cost of a run is at most 54/√a. Below a ≤ 3/4 the critical stage is the first with (6/5)^{l₀} > 1/sin 2θ, so (6/5)^{l₀} ≤ (6/5)/sin 2θ and sin 2θ ≥ √a; above it every stage already succeeds with probability ≥ a > 3/4.

Honest scope

The theorem is the upper bound of BHMT's Θ(1/√a); the matching lower bound is the optimality of Grover search (Bennett–Bernstein–Brassard–Vazirani), not treated here. The cost charged to a stage, 2 + 2j, is an upper bound on the applications actually used when the direct measurement already succeeds. The process model is an abstract probability space carrying the stage variables with the stated laws — the standard reading of "independent stages with fresh randomness"; its consistency is witnessed by exists_qsearchRun on the infinite product of the stage laws. Query counting is by applications of the abstract step, as in AmplitudeAmplification.lean; no gate decomposition is claimed. The constant 54 is not optimised (BHMT's own accounting gives a smaller one).

Source

Brassard, Høyer, Mosca, Tapp 2002, Quantum amplitude amplification and estimation, Contemp. Math. 305, Theorem 3 and the algorithm QSearch (§2, with c = 6/5), Lemma 2 (the engine, qsearch_average).

The schedule

noncomputable def QuantumInfo.qsearchRatio : ℝ

BHMT's growth constant, c = 6/5.

Equations

• QuantumInfo.qsearchRatio = 6 / 5

noncomputable def QuantumInfo.qsearchGuess (l : ℕ) : ℕ

The stage-l guess M_l = ⌈(6/5)^l⌉.

Equations

• QuantumInfo.qsearchGuess l = ⌈QuantumInfo.qsearchRatio ^ l⌉₊

theorem QuantumInfo.one_lt_qsearchRatio : 1 < qsearchRatio

theorem QuantumInfo.one_le_qsearchRatio_pow (l : ℕ) : 1 ≤ qsearchRatio ^ l

theorem QuantumInfo.le_qsearchGuess (l : ℕ) : qsearchRatio ^ l ≤ ↑(qsearchGuess l)

theorem QuantumInfo.qsearchGuess_pos (l : ℕ) : 0 < qsearchGuess l

theorem QuantumInfo.qsearchGuess_lt (l : ℕ) : ↑(qsearchGuess l) < qsearchRatio ^ l + 1

The stage success probability

noncomputable def QuantumInfo.stageProbAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (j : ℕ) : ℝ

The success probability of one stage at round count j: the direct measurement of ψ succeeds with probability a = goodProb G ψ; failing that, a fresh copy is amplified j rounds and measured.

Equations

• QuantumInfo.stageProbAt G ψ j = QuantumInfo.goodProb G ψ + (1 - QuantumInfo.goodProb G ψ) * QuantumInfo.goodProb G ((QuantumInfo.ampStep ψ G)^[j] ψ)

noncomputable def QuantumInfo.stageProb {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (M : ℕ) : ℝ

The success probability of a stage with guess M: the round count is uniform below M.

Equations

• QuantumInfo.stageProb G ψ M = (↑M)⁻¹ * ∑ j ∈ Finset.range M, QuantumInfo.stageProbAt G ψ j

theorem QuantumInfo.goodProb_iterate_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (j : ℕ) : goodProb G ((ampStep ψ G)^[j] ψ) ≤ 1

theorem QuantumInfo.stageProbAt_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha1 : goodProb G ψ < 1) (j : ℕ) : 0 ≤ stageProbAt G ψ j

theorem QuantumInfo.stageProbAt_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (j : ℕ) : stageProbAt G ψ j ≤ 1

theorem QuantumInfo.le_stageProbAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha1 : goodProb G ψ < 1) (j : ℕ) : goodProb G ψ ≤ stageProbAt G ψ j

The direct measurement alone: a stage succeeds with probability at least a.

theorem QuantumInfo.goodProb_iterate_le_stageProbAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (j : ℕ) : goodProb G ((ampStep ψ G)^[j] ψ) ≤ stageProbAt G ψ j

The amplified measurement alone: a stage succeeds at least as often as Q^j ψ does.

theorem QuantumInfo.stageProb_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha1 : goodProb G ψ < 1) (M : ℕ) : 0 ≤ stageProb G ψ M

theorem QuantumInfo.le_stageProb {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha1 : goodProb G ψ < 1) {M : ℕ} (hM : 0 < M) : goodProb G ψ ≤ stageProb G ψ M

A stage succeeds with probability at least a.

theorem QuantumInfo.quarter_le_stageProb {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (M : ℕ) (hM : 1 ≤ ↑M * (2 * √(goodProb G ψ * (1 - goodProb G ψ)))) : 1 / 4 ≤ stageProb G ψ M

★ The engine, in stage form (BHMT Lemma 2): once M · sin 2θ ≥ 1, a stage succeeds with probability at least 1/4.

The run as a random process

structure QuantumInfo.QSearchRun {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (M : ℕ → ℕ) {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : Type u_2

A run of QSearch as a random process. On a probability space (Ω, μ), stage l draws its round count J l and records its success W l. The stages are independent, J l is uniform below the guess M l, and given J l = j the stage succeeds with the Born probability stageProbAt G ψ j (the direct measurement, then the amplified one on a fresh copy).

• J : ℕ → Ω → ℕ

  The round count drawn at stage l.

• W : ℕ → Ω → Bool

  Whether stage l found a good element.

• measurable_J (l : ℕ) : Measurable (self.J l)

  The round counts are measurable.

• measurable_W (l : ℕ) : Measurable (self.W l)

  The outcomes are measurable.

• indep : ProbabilityTheory.iIndepFun (fun (l : ℕ) (ω : Ω) => (self.J l ω, self.W l ω)) μ

  The stages use fresh randomness.

• uniform (l j : ℕ) : μ (self.J l ⁻¹' {j}) = if j < M l then (↑(M l))⁻¹ else 0

  The round count is uniform below the guess.

• law (l j : ℕ) : μ (self.J l ⁻¹' {j} ∩ self.W l ⁻¹' {true}) = μ (self.J l ⁻¹' {j}) * ENNReal.ofReal (stageProbAt G ψ j)

  Given the round count, the stage succeeds with the Born probability.

def QuantumInfo.QSearchRun.reach {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : Set Ω

Stage l is reached: every earlier stage failed.

Equations

• R.reach l = ⋂ k ∈ Finset.range l, R.W k ⁻¹' {false}

theorem QuantumInfo.QSearchRun.measurableSet_W_false {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : MeasurableSet (R.W l ⁻¹' {false})

theorem QuantumInfo.QSearchRun.measurableSet_W_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : MeasurableSet (R.W l ⁻¹' {true})

theorem QuantumInfo.QSearchRun.measurableSet_J {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l j : ℕ) : MeasurableSet (R.J l ⁻¹' {j})

theorem QuantumInfo.QSearchRun.measurableSet_reach {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : MeasurableSet (R.reach l)

theorem QuantumInfo.QSearchRun.comap_W_false {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (k : ℕ) : MeasurableSet (R.W k ⁻¹' {false})

The failure event of stage k, seen through stage k's own variables.

theorem QuantumInfo.QSearchRun.comap_J {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (k j : ℕ) : MeasurableSet (R.J k ⁻¹' {j})

The round-count event of stage k, seen through stage k's own variables.

theorem QuantumInfo.QSearchRun.meas_reach {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : μ (R.reach l) = ∏ k ∈ Finset.range l, μ (R.W k ⁻¹' {false})

Reaching stage l: every earlier stage fails, independently.

theorem QuantumInfo.QSearchRun.meas_J_inter_reach {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l j : ℕ) : μ (R.J l ⁻¹' {j} ∩ R.reach l) = μ (R.J l ⁻¹' {j}) * μ (R.reach l)

The round count of stage l is independent of reaching stage l.

The cost

noncomputable def QuantumInfo.QSearchRun.stageCost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) (ω : Ω) : ENNReal

The applications of A and A⁻¹ charged to stage l if it is reached: one for the direct run, one for the fresh preparation and two per amplification round.

Equations

• R.stageCost l ω = (R.reach l).indicator (fun (ω : Ω) => 2 + 2 * ↑(R.J l ω)) ω

noncomputable def QuantumInfo.QSearchRun.cost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (ω : Ω) : ENNReal

The total cost of the run: the charges of every reached stage.

Equations

• R.cost ω = ∑' (l : ℕ), R.stageCost l ω

theorem QuantumInfo.QSearchRun.measurable_stageCost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) : Measurable (R.stageCost l)

theorem QuantumInfo.QSearchRun.lintegral_cost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) : ∫⁻ (ω : Ω), R.cost ω ∂μ = ∑' (l : ℕ), ∫⁻ (ω : Ω), R.stageCost l ω ∂μ

The expected cost is the sum of the expected stage costs.

theorem QuantumInfo.QSearchRun.sum_two_add_two_mul (M : ℕ) : ∑ j ∈ Finset.range M, (2 + 2 * j) = M * (M + 1)

∑_{j<M} (2 + 2j) = M (M + 1).

theorem QuantumInfo.QSearchRun.lintegral_stageCost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (l : ℕ) (hM : 0 < M l) : ∫⁻ (ω : Ω), R.stageCost l ω ∂μ = (↑(M l) + 1) * μ (R.reach l)

A reached stage costs M_l + 1 in expectation: the fresh draw is independent of the past, and a uniform round count below M has mean (M − 1)/2.

theorem QuantumInfo.QSearchRun.meas_W_false {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) [MeasureTheory.IsProbabilityMeasure μ] (l : ℕ) : μ (R.W l ⁻¹' {false}) = 1 - μ (R.W l ⁻¹' {true})

theorem QuantumInfo.QSearchRun.meas_W_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) (ha1 : goodProb G ψ < 1) (l : ℕ) (hM : 0 < M l) : μ (R.W l ⁻¹' {true}) = ENNReal.ofReal (stageProb G ψ (M l))

The stage law, averaged: stage l succeeds with probability stageProb G ψ (M l).

Past the critical stage

theorem QuantumInfo.QSearchRun.meas_reach_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {M : ℕ → ℕ} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (R : QSearchRun G ψ M μ) [MeasureTheory.IsProbabilityMeasure μ] (l₀ : ℕ) (hq : ∀ (k : ℕ), l₀ ≤ k → ENNReal.ofReal (1 / 4) ≤ μ (R.W k ⁻¹' {true})) (l : ℕ) : μ (R.reach l) ≤ ENNReal.ofReal (3 / 4) ^ (l - l₀)

Once every stage from l₀ on succeeds with probability at least 1/4, the probability of reaching stage l is at most (3/4)^{l − l₀}.

The series

noncomputable def QuantumInfo.qsearchWeight (l₀ l : ℕ) : ℝ

The geometric weights of the schedule: (5/6)^{l₀−l} up to the critical stage l₀, (9/10)^{l−l₀} after it.

Equations

• QuantumInfo.qsearchWeight l₀ l = if l ≤ l₀ then (5 / 6) ^ (l₀ - l) else (9 / 10) ^ (l - l₀)

theorem QuantumInfo.sum_qsearchWeight_le (l₀ N : ℕ) : ∑ l ∈ Finset.range N, qsearchWeight l₀ l ≤ 15

theorem QuantumInfo.qsearch_partial_sum_le (l₀ N : ℕ) : ∑ l ∈ Finset.range N, (↑(qsearchGuess l) + 1) * (3 / 4) ^ (l - l₀) ≤ 45 * qsearchRatio ^ l₀

The schedule series, bounded: every partial sum of (M_l + 1)(3/4)^{l − l₀} is at most 45 · (6/5)^{l₀}. Before the critical stage the terms are ≤ 3 c^l = 3 c^{l₀} (5/6)^{l₀−l}, after it ≤ 3 c^{l₀} (9/10)^{l−l₀}.

The expected cost

theorem QuantumInfo.QSearchRun.lintegral_cost_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (R : QSearchRun G ψ qsearchGuess μ) (l₀ : ℕ) (hq : ∀ (k : ℕ), l₀ ≤ k → ENNReal.ofReal (1 / 4) ≤ μ (R.W k ⁻¹' {true})) : ∫⁻ (ω : Ω), R.cost ω ∂μ ≤ ENNReal.ofReal (45 * qsearchRatio ^ l₀)

The expected cost past a critical stage: if every stage from l₀ on succeeds with probability at least 1/4, the expected cost is at most 45 · (6/5)^{l₀}.

theorem QuantumInfo.QSearchRun.qsearch_expected_cost {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (R : QSearchRun G ψ qsearchGuess μ) (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) : ∫⁻ (ω : Ω), R.cost ω ∂μ ≤ ENNReal.ofReal (54 / √(goodProb G ψ))

★★ BHMT Theorem 3, the upper bound. For a unit state with unknown success probability 0 < a < 1, a run of QSearch uses at most 54/√a applications of A and A⁻¹ in expectation. Below a ≤ 3/4 the critical stage l₀ is the first with (6/5)^{l₀} > 1/sin 2θ, past which every stage succeeds with probability ≥ 1/4; above it the direct measurement already succeeds with probability > 3/4 at every stage.

The model is consistent: a run on the product of the stage laws

noncomputable def QuantumInfo.stageMeasure (q : ℕ → ℝ) (M : ℕ) : MeasureTheory.Measure (ℕ × Bool)

The law of one stage with guess M and conditional success probabilities q: the round count j uniform below M, then success with probability q j.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumInfo.stageMeasure_apply (q : ℕ → ℝ) (M : ℕ) {S : Set (ℕ × Bool)} (hS : MeasurableSet S) : (stageMeasure q M) S = (↑M)⁻¹ * ∑ j ∈ Finset.range M, (ENNReal.ofReal (q j) * S.indicator 1 (j, true) + ENNReal.ofReal (1 - q j) * S.indicator 1 (j, false))

theorem QuantumInfo.stageMeasure_univ (q : ℕ → ℝ) (hq0 : ∀ (j : ℕ), 0 ≤ q j) (hq1 : ∀ (j : ℕ), q j ≤ 1) {M : ℕ} (hM : 0 < M) : (stageMeasure q M) Set.univ = 1

theorem QuantumInfo.stageMeasure_fst (q : ℕ → ℝ) (hq0 : ∀ (j : ℕ), 0 ≤ q j) (hq1 : ∀ (j : ℕ), q j ≤ 1) (M j : ℕ) : (stageMeasure q M) (Prod.fst ⁻¹' {j}) = if j < M then (↑M)⁻¹ else 0

The marginal of the round count: uniform below M.

theorem QuantumInfo.stageMeasure_singleton_true (q : ℕ → ℝ) (M j : ℕ) : (stageMeasure q M) {(j, true)} = if j < M then (↑M)⁻¹ * ENNReal.ofReal (q j) else 0

The joint law: round count j and success, with probability M⁻¹ q j.

theorem QuantumInfo.exists_qsearchRun {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (M : ℕ → ℕ) (hM : ∀ (l : ℕ), 0 < M l) : ∃ (μ : MeasureTheory.Measure (ℕ → ℕ × Bool)), MeasureTheory.IsProbabilityMeasure μ ∧ Nonempty (QSearchRun G ψ M μ)

★ The model is consistent. For every unit state with 0 < a < 1 and every schedule of positive guesses, the product of the stage laws over the stages carries a QSearchRun: the coordinates are independent (iIndepFun_infinitePi) and each has the stage law.