Neighborhoods of sets

Stream: Is there code for X?

[Vincent Beffara]

Do we have something like this?

import analysis.complex.basic
import data.set.prod

open filter metric set
open_locale topological_space big_operators

variables {K : set ℂ} {ε : ℝ}

def inflate (K : set ℂ) (ε : ℝ) : set ℂ := ⋃ z : K, ball z ε

def inflate' (K : set ℂ) (ε : ℝ) : set ℂ := ⋃ z : K, closed_ball z ε

lemma is_open_inflate : is_open (inflate K ε) :=
is_open_Union (λ z, is_open_ball)

lemma is_compact.is_compact_inflate' (hK : is_compact K) :
  is_compact (inflate' K ε) :=
begin
  suffices : (λ x : ℂ × ℂ, x.1 + x.2) '' K ×ˢ closed_ball (0 : ℂ) ε = inflate' K ε,
    from this ▸ is_compact.image (hK.prod (is_compact_closed_ball _ _)) (by continuity),
  ext z; split,
  { rintro ⟨⟨z₁, z₂⟩, ⟨h₁, h₂⟩, h₃⟩,
    exact mem_Union.mpr ⟨⟨z₁, h₁⟩, by simpa [← h₃] using h₂⟩ },
  { intro h,
    obtain ⟨⟨x, h₁⟩, h₂⟩ := mem_Union.mp h,
    refine ⟨⟨x, z - x⟩, ⟨h₁, by simpa [complex.dist_eq] using h₂⟩, by simp⟩ }
end

Mandatory #xy comment: my goal is to get a statement of differentiability of contour integral as a function of the contour, using has_deriv_at_integral_of_dominated_loc_of_lip, and ultimately to define primitives of holomorphic functions on star-like domains by

noncomputable def primitive (f : ℂ → ℂ) (z₀ : ℂ) : ℂ → ℂ :=
  λ z, (z - z₀) * ∫ t in 0..1, f (z₀ + t • (z - z₀))

[Yaël Dillies]

docs#metric.thickening, docs#metric.cthickening

[Yaël Dillies]

Also, I assume you know about docs#star_convex?

[Vincent Beffara]

That's my next step :-)

[Vincent Beffara]

While I'm asking : do we know that if a compact K is contained in an open set U then so is one of its cthickenings? That follows from continuity of the distance and feels like one more thing that @Sebastien Gouezel must have done at some point

[Yaël Dillies]

I think you can get there using docs#disjoint.exists_cthickenings (which I needed for geometric Hahn-Banach) by taking s := K, t := Uᶜ.

[Vincent Beffara]

Ah, indeed that's going to give it directly

[Vincent Beffara]

And while I am using zulip_search [yael] : do we know that the cthickening of a compact set is compact under realistic assumptions?

[Yaël Dillies]

:grinning: I think not. The closest we have seems to be docs#is_compact.cthickening_eq_bUnion_closed_ball, which brings you back to your definition ofinflate' above.

[Vincent Beffara]

Yes and then we know that finite bUnions of compact sets are compact but that's not enough. Since my use case is just the complex plane, I will just use metric.bounded.cthickening. Thanks again!

[Yaël Dillies]

#14926 for the lemma you suggested

[Vincent Beffara]

I got to this:

lemma star_convex.segment (U_star : star_convex ℝ z₀ U) (U_open : is_open U) (hz : z ∈ U) :
  ∃ δ : ℝ, 0 < δ ∧ cthickening δ (segment ℝ z₀ z) ⊆ U :=
begin
  have h1 : disjoint (segment ℝ z₀ z) Uᶜ,
    from disjoint_iff_subset_compl_right.mpr ((compl_compl U).symm ▸ (U_star.segment_subset hz)),
  obtain ⟨δ, δ_pos, h3⟩ := h1.exists_cthickenings is_compact_segment U_open.is_closed_compl,
  replace h3 := disjoint_iff_subset_compl_right.mp h3,
  exact ⟨δ, δ_pos, h3.trans (compl_subset_comm.mp (self_subset_cthickening Uᶜ))⟩
end

which is the special case for a segment. Will refactor to use your lemma at some point :-)

[Yaël Dillies]

@Vincent Beffara, you have it!