TerminalCounts.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual terminal indices and their counting cost

Terminals consist of prescribed points together with points flagged by two distinct grids. Their cardinality is bounded by the prescribed cardinality plus the number of pair/flag incidences. This upper counting cost is integrable and its expectation, scaled by the square of the spacing, tends to zero for the actual reciprocal-grid laws.

theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_active_of_weighted_count_ne_top line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.weighted_count_toReal_eq_ncard line 34
def OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalIndices line 51
def OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalCost line 58

theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_gridTerminalIndices_and_card_le line 65

Source documentation

Counting pair/point incidences only overcounts the actual terminal indices, including the prescribed finite set.

theorem finite_gridTerminalIndices_and_card_le {n : ℕ} {P S : Type*}
    (F : Set S) (hF : F.Finite) (h : ℝ)
    (pairs : P → Fin n × Fin n) (a b : Fin n → S → ℝ) (θ : Fin n → ℝ)
    (hfinite : gridCollisionCount h pairs a b θ ≠ ∞) :
    (gridTerminalIndices F h pairs a b θ).Finite ∧
      ((gridTerminalIndices F h pairs a b θ).ncard : ℝ) ≤
        gridTerminalCost F h pairs a b θ := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.gridCollisionCount, OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalIndices, OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalCost

theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_gridTerminalCost line 88
theorem OAI.CircleDomainRigidity.FiniteTransfer.gridTerminalCost_nonneg line 99

theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_gridTerminalCost_mean_tendsto_zero line 107

Source documentation

The finitely many prescribed terminals also have vanishing scaled expected cost. The number of pair/flag incidences was handled by the clipped-product summability estimate.

theorem scaled_gridTerminalCost_mean_tendsto_zero {n : ℕ} {P S : Type*}
    [Fintype P] [Countable S] (F : Set S)
    (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
    (a b : Fin n → S → ℝ) (hwidth : ∀ i s, 0 ≤ b i s - a i s)
    (hwidth2 : ∀ i, Summable (fun s => (b i s - a i s) ^ 2)) :
    Tendsto (fun N => reciprocalGridStep N ^ 2 *
      (∫ θ, gridTerminalCost F (reciprocalGridStep N) pairs a b θ
        ∂reciprocalGridLaw n N)) atTop (𝓝 0) := by
…

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

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_with_finite_terminals_and_good_widths line 134

Source documentation

Uniform wedge-mean bounds give spacing and shifts with a small terminal counting cost for every sufficiently narrow staircase.

theorem exists_grid_with_finite_terminals_and_good_widths
    {n : ℕ} {P S : Type*} [Fintype P] [Countable S]
    (F : Set S) (hF : F.Finite)
    (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
    (a b : Fin n → S → ℝ) (hwidth : ∀ i s, 0 ≤ b i s - a i s)
    (hwidth2 : ∀ i, Summable (fun s => (b i s - a i s) ^ 2))
    (W : ℕ → ℕ → (Fin n → ℝ) → ℝ) (Q : ℕ → (Fin n → ℝ) → Prop)
    {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ)
    (hWi : ∀ N k, Integrable (W N k) (reciprocalGridLaw n N))
    (hW0 : ∀ N k, ∀ᵐ θ ∂reciprocalGridLaw n N, 0 ≤ W N k θ)
    (hQ : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, Q N θ)
    (hWmean : ∀ᶠ N in atTop, ∀ k,
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridLaw