GridPreparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Preparing the actual random grid from finite-energy coordinates

The retained core, cutoff, cutoff energy and small original wedge sum are all constructed. The only grid event supplied to the selection is an explicitly conull event, as in the separate compatibility argument.

theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_planarGradient line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_coordinateWedges_eq_sum line 25

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_core_cutoff_and_grid line 42

Source documentation

Finite-energy smooth coordinates produce an actual core, cutoff, spacing, shifts, terminal-count estimate and frequently small modified wedge cost. No small-tail or cutoff-integrability premise is left over.

theorem exists_core_cutoff_and_grid
    {G K₀ : Set (ℝ × ℝ)} (hG : IsOpen G) (hK₀ : IsCompact K₀) (hK₀G : K₀ ⊆ G)
    {n : ℕ} (u : Fin n → (ℝ × ℝ) → ℝ) (huM : ∀ i, Measurable (u i))
    (hu : ∀ i, ContDiffOn ℝ ∞ (u i) G)
    (hu2 : ∀ i, MemLp (planarGradient (u i)) 2 (volume.restrict G))
    {S : Type*} [Countable S] (F : Set S) (hF : F.Finite) (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))
    (P : ℕ → (Fin n → ℝ) → Prop)
    (hP : ∀ N, ∀ᵐ θ ∂reciprocalGridLaw n N, P N θ)
    {η ρ : ℝ} (hη : 0 < η) (hρ : 0 < ρ) :
    ∃ (K L : Set (ℝ × ℝ)) (χ : (ℝ × ℝ) → ℝ) (N : ℕ) (θ : Fin n → ℝ),
…

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