ActualWedgeCost.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Grid selection for the actual cutoff coordinate differentials

All fixed-width spatial integrability follows from the original L² covectors. The selected random cost is exactly the integral of the unordered wedge sum of the actual modified scalar coordinates.

def OAI.CircleDomainRigidity.FiniteTransfer.cutoffCoordinateFamily line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoff_wedges_integrable_and_eq_cost line 26

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_for_actual_coordinate_wedges line 62

Source documentation

The selected spacing and shifts control actual coordinate gradients, and every width has an integrable spatial wedge sum.

theorem exists_grid_for_actual_coordinate_wedges
    {μ : Measure (ℝ × ℝ)} [SFinite μ] {n : ℕ} {S : Type*} [Countable S]
    (u : Fin n → (ℝ × ℝ) → ℝ) (χ : (ℝ × ℝ) → ℝ)
    (hu : ∀ i, Measurable (u i)) (hχ : Measurable χ)
    (hdu : ∀ i, Measurable (planarGradient (u i))) (hdχ : Measurable (planarGradient χ))
    (hu2 : ∀ i, MemLp (planarGradient (u i)) 2 μ) (hχ2 : MemLp (planarGradient χ) 2 μ)
    (hd : ∀ᵐ z ∂μ, DifferentiableAt ℝ χ z ∧ ∀ i, DifferentiableAt ℝ (u i) z)
    (hχ0 : ∀ z, 0 ≤ χ z) (hχ1 : ∀ z, χ z ≤ 1)
    (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))
    (Q : ℕ → (Fin n → ℝ) → Prop)
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient