OAI/Analysis/CircleDomains/Sobolev/ClosedGapIntegrals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual closed gaps have disjoint interiors; positive hole widths make the closed gaps disjoint too. Their density integrals use at most the density integral on the whole source segment.

  1. theorem OAI.CircleDomainRigidity.closed_gaps_disjoint line 14
  2. theorem OAI.CircleDomainRigidity.closed_gap_integrals_le line 32
  3. theorem OAI.CircleDomainRigidity.closed_gap_integrals_le_of_nonstrict line 44

    Source documentation

    Singleton endpoints have zero length, so even zero-width holes permit summing the closed-gap integrals without double payment.

     theorem closed_gap_integrals_le_of_nonstrict {n : ℕ} (a b : ℝ) (H : Fin n → ℝ × ℝ)
    (hvalid : ∀ i, (H i).1 ≤ (H i).2) (hfirst : Monotone (fun i => (H i).1))
    {B V : Set ℝ} (hB : MeasurableSet B) (hV : MeasurableSet V)
    {ρ : ℝ → ℝ} (hi : IntegrableOn ρ B volume) (hρ : ∀ x ∈ B, 0 ≤ ρ x)
    (hsub : ∀ i, Icc (gapsAfterHoles a b H i).1 (gapsAfterHoles a b H i).2 ∩ V ⊆ B) :
    (∑ i, ∫ x in Icc (gapsAfterHoles a b H i).1 (gapsAfterHoles a b H i).2 ∩ V, ρ x) ≤
      ∫ x in B, ρ x := by
…

    Mentions: OAI.CircleDomainRigidity.gapsAfterHoles