OAI/Analysis/CircleDomains/Modulus/FiniteWedgeCosts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CircleDomainRigidity.FiniteTransfer.staircaseWidth line 19
2. theorem OAI.CircleDomainRigidity.FiniteTransfer.staircaseWidth_pos line 22
3. theorem OAI.CircleDomainRigidity.FiniteTransfer.staircaseWidth_lt line 25
4. theorem OAI.CircleDomainRigidity.FiniteTransfer.staircaseWidth_tendsto_zero line 32
5. def OAI.CircleDomainRigidity.FiniteTransfer.staircasePairCost line 37
6. def OAI.CircleDomainRigidity.FiniteTransfer.staircaseWedgeCost line 44
7. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_staircasePairCost line 50
8. theorem OAI.CircleDomainRigidity.FiniteTransfer.staircaseWedgeCost_nonneg line 68
9. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_staircaseWedgeCost_and_mean_le line 77

   Source documentation

   The finite-list mean estimate, with no joint-integrability premise. The original pairwise wedges and cutoff correction terms suffice.

   theorem integrable_staircaseWedgeCost_and_mean_le
       {X P : Type*} [MeasurableSpace X] [Fintype P] {μ : Measure X} [SFinite μ] {n : ℕ}
       (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
       (u : Fin n → X → ℝ × ℝ) (c : X → ℝ × ℝ) (x : Fin n → X → ℝ) (χ : X → ℝ)
       (hu : ∀ i, Measurable (u i)) (hc : Measurable c)
       (hx : ∀ i, Measurable (x i)) (hχ : Measurable χ)
       {h δ : ℝ} (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
       (hχ0 : ∀ z, 0 ≤ χ z) (hχ1 : ∀ z, χ z ≤ 1)
       (hbase : ∀ p, Integrable (fun z => |planarWedge (u (pairs p).1 z) (u (pairs p).2 z)|) μ)
       (herr : ∀ p, Integrable (fun z => |planarWedge (u (pairs p).1 z) (c z)| +
         |planarWedge (c z) (u (pairs p).2 z)|) μ) :
       Integrable (staircaseWedgeCost μ pairs u c x χ h δ)
   …

   Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge, OAI.CircleDomainRigidity.FiniteTransfer.staircaseWedgeCost

10. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_for_actual_wedge_cost line 120

    Source documentation

    The grid-selection stage with the actual constructed wedge cost, actual terminal set, and explicit sequence of widths tending to zero. Its spatial hypotheses are the original square-integrable covectors and a small original wedge sum outside the retained core.

    theorem exists_grid_for_actual_wedge_cost
        {X P S : Type*} [MeasurableSpace X] [Fintype P] [Countable S]
        {μ : Measure X} [SFinite μ] {n : ℕ}
        (pairs : P → Fin n × Fin n) (hpairs : ∀ p, (pairs p).1 ≠ (pairs p).2)
        (u : Fin n → X → ℝ × ℝ) (c : X → ℝ × ℝ) (x : Fin n → X → ℝ) (χ : X → ℝ)
        (hu : ∀ i, Measurable (u i)) (hc : Measurable c)
        (hx : ∀ i, Measurable (x i)) (hχ : Measurable χ)
        (hu2 : ∀ i, MemLp (u i) 2 μ) (hc2 : MemLp c 2 μ)
        (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))
    …