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!

[Josha Dekker]

In Mathlib, nhds, reflects to the neighborhood filter. However, I'm wondering if we have the definition of a neighborhood, as defined in Bourbaki, General Topology:

• a set B is a neighborhood of a set A is a neighborhood of a set A if it contains an open cover of A (or an open set that contains A)
• a set B is a neighborhood of a point x if it is a neighborhood of {x}
  This came up as I'm working on getting the first few definitions of Bourbaki in https://github.com/JADekker/LeanBourbaki, in the effort to link the results in that book to Mathlib.

[Yaël Dillies]

Is that not literally B ∈ 𝓝 A?

[Yaël Dillies]

The docstring of docs#nhds claims so

[Yaël Dillies]

Sorry, nhds is the filter of neighborhoods of a point. nhdsSet is the filter of neighborhoods of a set.

[Josha Dekker]

Yaël Dillies said:

Is that not literally B ∈ 𝓝 A?

Yes, it is. I was just wondering if we had a definition, but that is probably not necessary for that project of course, such small statements are fine as well

[Sébastien Gouëzel]

Yes, we have it, it's 𝓝ˢ A.

[Yaël Dillies]

We do not have a standalone predicate, if that's what you asked.

[Josha Dekker]

Yaël Dillies said:

We do not have a standalone predicate, if that's what you asked.

Yes. That is what I meant! Thanks!

[Patrick Massot]

What would such a predicate buy you?

[Josha Dekker]

Patrick Massot said:

What would such a predicate buy you?

Nothing in Mathlib. In the above project, the goal is to link each result in Bourbaki’s General Topology to a result in Mathlib, to create a reference for the results. I didn’t want to miss this predicate if it was there, that’s why I asked!

[Patrick Massot]

I think

neighborhood of a set:
  title: 'Neighborhood of a set'
  decl: 'A ∈ 𝓝ˢ B'
  comment: 'In mathlib, neighborhoods of sets do not have their own predicate. A set A is a
    neighborhood of a set B if it lies in the neighborhood-of-sets filter 𝓝ˢ B'
  reference: 'Definition 1.4'

[Patrick Massot]

is not great since it cannot be turned into a link to source code

[Josha Dekker]

Patrick Massot said:

is not great since it cannot be turned into a link to source code

Would something like using ‘nhdsSet’ in the ‘decl’ and writing what I have now as a comment be better?

[Patrick Massot]

Yes.

[Josha Dekker]

Thank you, this is very helpful in getting the format right!

[Patrick Massot]

There will definitely be cases where a single decl won’t be enough.

[Josha Dekker]

Patrick Massot said:

There will definitely be cases where a single decl won’t be enough.

Yeah, we will have to see how that plays out, perhaps multiple declarations or comma-separated ones will work. I've updated the file now.