GridSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting a compatible grid with small costs

This is the numerical selection step in 047-02, Section 2. A small expected wedge cost and a terminal count whose scaled expectation tends to zero give a positive grid spacing and a compatible sample for which both realized costs are small. The random staircase and its compatibility conditions are explicit hypotheses of this selection theorem.

theorem OAI.CircleDomainRigidity.FiniteTransfer.scaled_terminal_mean_tendsto_zero_of_bound line 23

Source documentation

The terminal expectation tends to zero after multiplication by h² when it is bounded by the finite clipped-product estimate from the paper.

theorem scaled_terminal_mean_tendsto_zero_of_bound
    {X κ τ ι : Type*} [MeasurableSpace X] {μ : Measure X}
    (J : ℝ → X → ℝ) (F : Finset κ) (P : Finset τ) (a b : τ → ι → ℝ)
    (ha : ∀ p ∈ P, ∀ s, 0 ≤ a p s) (hb : ∀ p ∈ P, ∀ s, 0 ≤ b p s)
    (ha2 : ∀ p ∈ P, Summable (fun s => a p s ^ 2))
    (hb2 : ∀ p ∈ P, Summable (fun s => b p s ^ 2))
    (hJ0 : ∀ h, 0 < h → ∀ᵐ x ∂μ, 0 ≤ J h x)
    (hbound : ∀ᶠ h : ℝ in 𝓝[>] 0,
      h ^ 2 * (∫ x, J h x ∂μ) ≤ h ^ 2 * (F.card : ℝ) +
        ∑ p ∈ P, ∑' s, min h (a p s) * min h (b p s)) :
    Tendsto (fun h : ℝ => h ^ 2 * (∫ x, J h x ∂μ)) (𝓝[>] 0) (𝓝 0) := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compatible_good_grid line 45

Source documentation

Choose an arbitrarily small positive grid spacing and a compatible sample with wedge cost below η and scaled square-root terminal count below η. The probability-space event may encode all compatibility conditions needed by the geometric construction.

theorem exists_compatible_good_grid {X : Type*} [MeasurableSpace X]
    {μ : Measure X} [IsProbabilityMeasure μ]
    (W J : ℝ → X → ℝ) (P : ℝ → X → Prop) {η δ : ℝ}
    (hη : 0 < η) (hδ : 0 < δ)
    (hWi : ∀ h, 0 < h → Integrable (W h) μ)
    (hJi : ∀ h, 0 < h → Integrable (J h) μ)
    (hW0 : ∀ h, 0 < h → ∀ᵐ x ∂μ, 0 ≤ W h x)
    (hJ0 : ∀ h, 0 < h → ∀ᵐ x ∂μ, 0 ≤ J h x)
    (hP : ∀ h, 0 < h → ∀ᵐ x ∂μ, P h x)
    (hWmean : ∀ᶠ h : ℝ in 𝓝[>] 0, (∫ x, W h x ∂μ) < η / 4)
    (hJmean : Tendsto (fun h : ℝ => h ^ 2 * (∫ x, J h x ∂μ))
      (𝓝[>] 0) (𝓝 0)) :
…