ReciprocalGridSelection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Selecting an actual reciprocal-integer grid

The grid spacing must be 1/N so that the staircases respect period one. The laws of the uniform shifts change with the spacing. This selection uses those actual product laws, keeps any prescribed conull compatibility event, and makes both the wedge cost and scaled terminal count small.

def OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep line 21
def OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep_pos line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep_le_one line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep_mul_denominator line 35
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep_tendsto_zero line 40
theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw_isProbabilityMeasure line 44

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_actual_compatible_good_grid line 52

Source documentation

Simultaneous selection with the exact laws and exact reciprocal spacings used in finite transfer.

theorem exists_actual_compatible_good_grid {n : ℕ}
    (W J : ℕ → (Fin n → ℝ) → ℝ) (P : ℕ → (Fin n → ℝ) → Prop)
    {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ)
    (hWi : ∀ N, Integrable (W N) (reciprocalGridLaw n N))
    (hJi : ∀ N, Integrable (J N) (reciprocalGridLaw n N))
    (hW0 : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, 0 ≤ W N θ)
    (hJ0 : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, 0 ≤ J N θ)
    (hP : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, P N θ)
    (hWmean : ∀ᶠ N in atTop, (∫ θ, W N θ ∂reciprocalGridLaw n N) < η / 4)
    (hJmean : Tendsto
      (fun N => reciprocalGridStep N ^ 2 * (∫ θ, J N θ ∂reciprocalGridLaw n N))
      atTop (𝓝 0)) :
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep