QuantumCore.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Exact integer arithmetic for the prescribed-mass order trial. These are dependencies of the actual main theorem, not assumptions about an unknown order and not a replacement target.

def OAI.ExactQuantumFactoring.OrderTrial.sampleCount line 16
Source documentation
Number of integers x<Q congruent to t modulo d, when t<d≤Q.
```
def sampleCount (Q d t : ℕ) : ℕ := (Q-1-t)/d+1
```
lemma OAI.ExactQuantumFactoring.OrderTrial.sampleCount_bounds line 18
lemma OAI.ExactQuantumFactoring.OrderTrial.lt_sampleCount_iff line 28
lemma OAI.ExactQuantumFactoring.OrderTrial.sum_progression line 35
def OAI.ExactQuantumFactoring.OrderTrial.bin line 59
Source documentation
Literal nearest-bin rule floor(jQ/d+1/2), expressed entirely with integers.
```
def bin (Q d j : ℕ) : ℕ := (2*j*Q+d)/(2*d)
```
def OAI.ExactQuantumFactoring.OrderTrial.binError line 61
lemma OAI.ExactQuantumFactoring.OrderTrial.binError_bound line 63
def OAI.ExactQuantumFactoring.OrderTrial.triangle line 95
Source documentation
Real triangular wave, period one; quotient norm makes continuity explicit.
```
noncomputable def triangle (x : ℝ) : ℝ := 1 - 4 * ‖(x : UnitAddCircle)‖
```
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_local line 97
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_add_int line 101
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_half line 106
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_continuous line 124
def OAI.ExactQuantumFactoring.OrderTrial.phase line 129
Source documentation
Exact polygon phase, with clockwise orientation as in the forward shift.
```
noncomputable def phase (x : ℝ) : ℂ := ⟨triangle x, -triangle (x - 1/4)⟩
```
Mentions: OAI.ExactQuantumFactoring.OrderTrial.triangle
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_continuous line 131
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_quarter line 140
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_add_int line 149
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_zero_quarter line 155
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_quadratic_lower line 169
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_add_quarters line 177
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_interpolates line 202
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_norm_le line 211
lemma OAI.ExactQuantumFactoring.OrderTrial.triangle_sub_le line 229
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_norm_sub_le line 242
lemma OAI.ExactQuantumFactoring.OrderTrial.phase_lipschitz line 253
lemma OAI.ExactQuantumFactoring.OrderTrial.segment_phase_sub_le line 258
lemma OAI.ExactQuantumFactoring.OrderTrial.centered_quadratic_integral line 264
lemma OAI.ExactQuantumFactoring.OrderTrial.centered_integral_re_lower line 278
def OAI.ExactQuantumFactoring.OrderTrial.averagePhase line 299
Source documentation
The normalized interval average appearing in the dyadic majorant.
```
noncomputable def averagePhase (a η : ℝ) : ℂ :=
…
```
lemma OAI.ExactQuantumFactoring.OrderTrial.averagePhase_lower line 302
lemma OAI.ExactQuantumFactoring.OrderTrial.averagePhase_upper line 328
def OAI.ExactQuantumFactoring.OrderTrial.residueIntegral line 335
Source documentation
I(u) in equation (majorant-integral), without a restriction on u needed for its analytic bounds.
```
noncomputable def residueIntegral (d : ℕ) (u η : ℝ) : ℂ :=
…
```
lemma OAI.ExactQuantumFactoring.OrderTrial.residueIntegral_bounds line 338

lemma OAI.ExactQuantumFactoring.OrderTrial.rectangle_error line 354

Source documentation

Quantitative rectangle rule with exactly the constant required in (majorant-integral-bounds).

lemma rectangle_error {f : ℝ → ℂ} (hf : Continuous f)
    (hL : ∀ v w, ‖f v-f w‖ ≤ 4*|v-w|) (a : ℝ) {h : ℝ} (hh : 0 ≤ h) :
    ‖h • f a - ∫ v in a..a+h, f v‖ ≤ 2*h^2 := by
…

lemma OAI.ExactQuantumFactoring.OrderTrial.rectangle_sum_error line 385
lemma OAI.ExactQuantumFactoring.OrderTrial.integral_endpoint_error line 406
lemma OAI.ExactQuantumFactoring.OrderTrial.rectangle_sum_unit_error line 427