BandGroupSampling.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Executable shared group estimates

All dyadic powers in the prescribed closed range are enumerated, including negative exponents. A scale is evaluated exactly when its sample count reaches the child count; otherwise one shared array of uniform labels is used for every member of the group. The selected member is the first minimizer in the fixed list order.

theorem OAI.EditApproximation.integerClosedRange_mem line 24
theorem OAI.EditApproximation.integerClosedRange_nodup line 35
theorem OAI.EditApproximation.groupDyadicScales_mem line 43
theorem OAI.EditApproximation.groupDyadicScales_nodup line 64
theorem OAI.EditApproximation.groupDyadicScales_pos line 68
theorem OAI.EditApproximation.groupDyadicScales_length line 75
theorem OAI.EditApproximation.groupDyadicScales_length_dyadic line 80
theorem OAI.EditApproximation.groupSampleCount_pos line 96
theorem OAI.EditApproximation.groupSampleCount_sampled line 101
theorem OAI.EditApproximation.groupScaleEstimate_exact line 114

theorem OAI.EditApproximation.groupScaleEstimate_normalized line 120

Source documentation

The sample and actual scale cost have exactly the normalized average used in the published Bernstein specialization.

theorem groupScaleEstimate_normalized {M b k : ℕ} (h : ℚ)
    (envelope value : Fin M → ℚ) (draw : Fin k → Fin M)
    (hM : 0 < M) (hb : 0 < b) (hk : 0 < k) (hsampled : k ≠ M) :
    ((groupScaleEstimate k h envelope value draw - groupScaleTrueCost h envelope value : ℚ) : ℝ) =
      (b : ℝ) * ((∑ j, normalizedChildSample (b : ℝ) (h : ℝ)
        (fun i => (envelope i : ℝ)) (fun i => (value i : ℝ)) (draw j)) / k -
          uniformMean (normalizedChildSample (b : ℝ) (h : ℝ)
            (fun i => (envelope i : ℝ)) (fun i => (value i : ℝ)))) := by
…

Mentions: OAI.EditApproximation.groupScaleEstimate, OAI.EditApproximation.groupScaleTrueCost, OAI.EditApproximation.normalizedChildSample, OAI.EditApproximation.uniformMean

theorem OAI.EditApproximation.selectGroupMember_spec line 151

Source documentation

Fixed ordered minimization; negating the rational estimate turns the finite maximum operation into the first cost minimum.

theorem selectGroupMember_spec {ι : Type*} (members : List ι) (hnonempty : members ≠ [])
    (estimate : ι → ℚ) :
    selectGroupMember members hnonempty estimate ∈ members ∧
      ∀ member ∈ members, estimate (selectGroupMember members hnonempty estimate) ≤ estimate member := by
…

Mentions: OAI.EditApproximation.selectGroupMember

theorem OAI.EditApproximation.groupScaleEstimate_concentration line 166
def OAI.EditApproximation.groupSharedDrawLaw line 225
instance OAI.EditApproximation.groupSharedDrawLaw_isProbabilityMeasure line 231
theorem OAI.EditApproximation.groupSharedDraw_projection line 237

theorem OAI.EditApproximation.selectGroupMember_cost_le line 254

Source documentation

Actual shared draws are reused for all group members at this scale; no independence between representatives is imposed.

theorem selectGroupMember_cost_le {ι : Type*} (members : List ι) (hnonempty : members ≠ [])
    (cost estimate : ι → ℚ) (specified : ι) (hspecified : specified ∈ members) (error : ℚ)
    (haccurate : ∀ member ∈ members, |estimate member - cost member| ≤ error) :
    cost (selectGroupMember members hnonempty estimate) ≤ cost specified + 2 * error := by
…

Mentions: OAI.EditApproximation.selectGroupMember

theorem OAI.EditApproximation.groupScaleTrueCost_sum line 268
theorem OAI.EditApproximation.uniform_sample_average_integral line 281
theorem OAI.EditApproximation.groupScaleEstimate_integral line 297
theorem OAI.EditApproximation.groupMemberEstimate_error line 317
theorem OAI.EditApproximation.testUnskippedBand_accept line 338
theorem OAI.EditApproximation.testUnskippedBand_center line 346
theorem OAI.EditApproximation.unskippedBandList_mem_iff line 357
theorem OAI.EditApproximation.unskippedBand_envelope_scale line 369
theorem OAI.EditApproximation.unskippedBand_rounded_value_bounds line 383
theorem OAI.EditApproximation.unskippedGroupEstimate_error line 403

theorem OAI.EditApproximation.unskippedGroupEstimate_failure line 425

Source documentation

Uniform simultaneous accuracy for the actual fixed list of unskipped records. The same per-scale samples are reused by every record.

theorem unskippedGroupEstimate_failure {T : ℕ} [NeZero M]
    [MeasurableSpace (Fin M)] [MeasurableSingletonClass (Fin M)]
    (scales : Fin T → ℚ) (count : Fin T → ℕ) (Q : ℕ)
    (hscales : List.ofFn scales = groupDyadicScales M b F)
    (hcount : ∀ scale, count scale = groupSampleCount M Q b (scales scale))
    (value : Fin M → TargetInterval target.length → ℚ)
    (members : List (UnskippedBand source target parent b P thetaExponent tau F child initial))
    (hM : 0 < M) (hQ : 0 < Q) (hb : 0 < b) (hF : 0 < F)
    (L0 : ℚ) (hL0 : 0 ≤ L0)
    (hsmall : 2 * L0 * (2 : ℚ) ^ (-(thetaExponent : ℤ)) ≤ 1)
    (hspatial : ∀ i s t, initial i s ≤ initial i t + L0 * targetEndpointDistance s t)
    (hvalue : ∀ i s, 0 ≤ value i s ∧ value i s ≤ initial i s)
…

Mentions: OAI.EditApproximation.groupDyadicScales, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.targetEndpointDistance

theorem OAI.EditApproximation.chooseUnskippedGroup_spec line 520
theorem OAI.EditApproximation.chooseUnskippedGroup_cost_le line 532