Using partitions of unity

Stream: maths

[Patrick Massot]

In the sphere eversion project we reached the point where we'll need to actually use partitions of unity. But either I'm not looking at the right place or the API isn't here. @Yury G. Kudryashov @Sebastien Gouezel @Heather Macbeth do you know how to finish the proof below? Or do you have useful pointers or advice?

import geometry.manifold.partition_of_unity

open_locale topological_space filter manifold big_operators
open set function filter

variables
  {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
  {F : Type*} [normed_group F] [normed_space ℝ F]


lemma partition_induction_on
  {P : E → F → Prop} (hP : ∀ x, convex ℝ {y | P x y})
  {n : with_top ℕ}
  (hP' : ∀ x : E, ∃ U ∈ 𝓝 x, ∃ f : E → F, cont_diff_on ℝ n f U ∧ ∀ x ∈ U, P x (f x)) :
  ∃ f : E → F, cont_diff ℝ n f ∧ ∀ x, P x (f x) :=
begin
  choose U hU hU' using hP',
  choose φ hφ using hU',
  rcases smooth_bump_covering.exists_is_subordinate 𝓘(ℝ, E) is_closed_univ (λ x h, hU x) with
    ⟨ι, b, hb⟩,
  let ρ := b.to_smooth_partition_of_unity,
  have sum_ρ := λ x, ρ.sum_eq_one (mem_univ x),
  have nonneg_ρ := ρ.nonneg,
  have lf : locally_finite (λ (i : ι), support (λ x, ρ i x • φ (b.c i) x)),
  { refine ρ.locally_finite.subset (λ i x hx hx', hx _),
    dsimp only,
    rw [hx', zero_smul] },
  refine ⟨λ x : E, (∑ᶠ i, (ρ i x) • φ (b.c i) x), cont_diff_iff_cont_diff_at.mpr _, _⟩,
  all_goals {
    intros x,
    rcases lf x with ⟨V, V_in : V ∈ 𝓝 x,
                      hV : {i : ι | (support (λ x, ρ i x • φ (b.c i) x) ∩ V).nonempty}.finite⟩},
  { sorry },
  { have := λ i, (hφ $ b.c i).2,
    sorry },
end

/-
-- Extra credit for a version in an open set:

lemma partition_induction_on {s : set E} (hs : is_open s)
  {P : E → F → Prop} (hP : ∀ x ∈ s, convex ℝ {y | P x y})
  {n : with_top ℕ}
  (hP' : ∀ x ∈ s, ∃ U ∈ 𝓝 x, ∃ f : E → F, cont_diff_on ℝ n f U ∧ ∀ x ∈ U, P x (f x)) :
  ∃ f : E → F, cont_diff_on ℝ n f s ∧ ∀ x ∈ s, P x (f x) :=
-/


example {f : E → ℝ} (h : ∀ x : E, ∃ U ∈ 𝓝 x, ∃ ε : ℝ, ∀ x' ∈ U, 0 < ε ∧ ε ≤ f x') :
  ∃ f' : E → ℝ, cont_diff ℝ ⊤ f' ∧ ∀ x, (0 < f' x ∧ f' x ≤ f x) :=
begin
  let P : E → ℝ → Prop := λ x t, 0 < t ∧ t ≤ f x,
  have hP : ∀ x, convex ℝ {y | P x y}, from λ x, convex_Ioc _ _,
  apply partition_induction_on hP,
  intros x,
  rcases h x with ⟨U, U_in, ε, hU⟩,
  exact ⟨U, U_in, λ x, ε, cont_diff_on_const, hU⟩
end

[Patrick Massot]

I should also ping @Oliver Nash and @Floris van Doorn

[Patrick Massot]

Note that the proof start may be wrong, I'm guessing part of the API there.

[Yury G. Kudryashov]

In about 9h I'll be home alone, then I'll try to prove it

[Oliver Nash]

I should add that I was using partitions of unity last week and I was delighted with what we have and I'm very grateful to Yury, Sébastien and others for what we have.

[Oliver Nash]

However I agree with Patrick: there is still some API to be added. I have some pieces locally (abstracted from very messy proofs that I bashed into the Sphere Eversion project) which I'll try to PR soon.

[Oliver Nash]

For the sake of definiteness, here is a result I found useful. I've tidied up the statement but still have to fix its ridiculous proof:

import topology.partition_of_unity

namespace partition_of_unity

open_locale topological_space big_operators
open function set

variables {ι X : Type*} {U : ι → set X} {s : set X} [topological_space X] (ho : ∀ i, is_open (U i))
variables (p : partition_of_unity ι X s) (hp : p.is_subordinate U)
include ho hp

lemma exists_finset_nhd (x : X) :
  ∃ (is : finset ι) {n : set X} (hn₁ : n ∈ 𝓝 x) (hn₂ : n ⊆ ⋂ i ∈ is, U i), ∀ (z ∈ n),
    support (λ i, p i z) ⊆ is :=
begin
  -- Ridiculous proof
  obtain ⟨n, hn, hn'⟩ := p.locally_finite x,
  classical,
  let is := hn'.to_finset.filter (λ i, x ∈ U i),
  let js := hn'.to_finset.filter (λ j, x ∉ U j),
  refine ⟨is, n ∩ (⋂ j ∈ js, (tsupport (p j))ᶜ) ∩ (⋂ i ∈ is, U i),
    filter.inter_mem (filter.inter_mem hn _) _, inter_subset_right _ _, λ z hz, _⟩,
  { refine (filter.bInter_finset_mem js).mpr (λ j hj, is_closed.compl_mem_nhds
      (is_closed_tsupport _) _),
    simp only [finset.mem_filter, finite.mem_to_finset, mem_set_of_eq] at hj,
    exact set.not_mem_subset (hp j) hj.2, },
  { refine (filter.bInter_finset_mem is).mpr (λ i hi, _),
    simp only [finset.mem_filter, finite.mem_to_finset, mem_set_of_eq] at hi,
    exact (ho i).mem_nhds hi.2, },
  { have hz' : z ∈ n,
    { rw inter_assoc at hz,
      exact mem_of_mem_inter_left hz, },
    have h₁ : support (λ i, p i z) ⊆ hn'.to_finset,
    { simp only [finite.coe_to_finset, mem_set_of_eq],
      exact λ i hi, ⟨z, mem_inter hi hz'⟩, },
    have hz₂ : ∀ j ∈ hn'.to_finset, j ∈ js → z ∉ support (p j),
    { rintros j - hj,
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz),
      simp only [finset.mem_filter, finite.mem_to_finset, mem_set_of_eq, mem_Inter, mem_compl_eq,
        and_imp] at hz,
      simp only [finset.mem_filter, finite.mem_to_finset, mem_set_of_eq] at hj,
      exact set.not_mem_subset (subset_tsupport (p j)) (hz j hj.1 hj.2), },
    intros i hi,
    suffices : i ∉ js,
    { simp only [finset.mem_filter, not_and, not_not_mem] at this,
      simp only [finset.coe_filter, finite.coe_to_finset, sep_set_of, mem_set_of_eq],
      refine ⟨_, this (h₁ hi)⟩,
      specialize h₁ hi,
      simpa using h₁, },
    exact λ contra, hz₂ i (h₁ hi) contra hi, },
end

end partition_of_unity

[Patrick Massot]

@Yury G. Kudryashov I'm currently proving my lemma so you don't need to worry about it.

[Yury G. Kudryashov]

Note that you can use docs#smooth_partition_of_unity.exists_is_subordinate instead of going through a smooth_bump_covering.

[Yury G. Kudryashov]

Anyway, if you're on it, then I'll wait.

[Patrick Massot]

I was on it but the administrative issues interfered so I'll have to come back to it

[Patrick Massot]

In the end there was too much admin and now I need to go and take care of kids. I'll return to this tonight if you don't do it in the mean time. I started a proof, but I wasn't careful enough it needs more information (see the comment at the end).

import geometry.manifold.partition_of_unity

noncomputable theory

open_locale topological_space filter manifold big_operators
open set function filter

variables
  {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
  {F : Type*} [normed_group F] [normed_space ℝ F]

lemma finsum.exists_finset {ι : Sort*} {X : Type*} [topological_space X] {E : Type*} [add_comm_monoid E]
{f : ι → X → E} (hf : locally_finite $ λ i, support (f i)) (x₀ : X) :
  ∃ s : finset ι, (λ x, ∑ᶠ i, f i x) =ᶠ[𝓝 x₀] λ x, ∑ i in s, f i x :=
begin
  rcases hf x₀ with ⟨V, V_in : V ∈ 𝓝 x₀,
                      hV : {i : ι | (support (f i) ∩ V).nonempty}.finite⟩,
  use hV.to_finset,
  filter_upwards [V_in],
  intros x x_in,
  apply finsum_eq_sum_of_support_subset,
  intros i hi,
  rw [finite.coe_to_finset],
  exact ⟨x, λ H, hi H, x_in⟩
end


lemma has_fderiv_at_of_not_mem (𝕜 : Type*) {E : Type*} {F : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 F]
  {f : E → F} {x} (hx : x ∉ tsupport f) : has_fderiv_at f (0 : E →L[𝕜] F) x :=
(has_fderiv_at_const (0 : F)  x).congr_of_eventually_eq
  (not_mem_closure_support_iff_eventually_eq.mp hx)

lemma cont_diff_at_of_not_mem (𝕜 : Type*) {E : Type*} {F : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 F]
  {f : E → F} {x} (hx : x ∉ tsupport f) (n : with_top ℕ) : cont_diff_at 𝕜 n f x :=
(cont_diff_at_const : cont_diff_at 𝕜 n (λ x, (0 : F)) x).congr_of_eventually_eq
   (not_mem_closure_support_iff_eventually_eq.mp hx)

-- TODO: put reasonnable assumptions and prove it
lemma tsupport_smul {𝕜 : Type*} {E : Type*} {F : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 F]
  (f : E → F) (s : E → 𝕜) : tsupport (λ x, s x • f x) ⊆ tsupport s :=
begin

  sorry
end

lemma partition_induction_on
  {P : E → F → Prop} (hP : ∀ x, convex ℝ {y | P x y})
  {n : with_top ℕ}
  (hP' : ∀ x : E, ∃ U ∈ 𝓝 x, ∃ f : E → F, cont_diff_on ℝ n f U ∧ ∀ x ∈ U, P x (f x)) :
  ∃ f : E → F, cont_diff ℝ n f ∧ ∀ x, P x (f x) :=
begin
  replace hP' : ∀ x : E, ∃ U ∈ 𝓝 x, is_open U ∧ ∃ f : E → F, cont_diff_on ℝ n f U ∧ ∀ x ∈ U, P x (f x),
  { intros x,
    rcases ((nhds_basis_opens x).exists_iff _).mp (hP' x) with ⟨U, ⟨x_in, U_op⟩, f, hf, hfP⟩,
    exact ⟨U, U_op.mem_nhds x_in, U_op, f, hf, hfP⟩,
    rintros s t hst ⟨f, hf, hf'⟩,
    exact ⟨f, hf.mono hst, λ x hx, hf' x (hst hx)⟩ },
  choose U hU U_op hU' using hP',
  choose φ hφ using hU',
  rcases smooth_bump_covering.exists_is_subordinate 𝓘(ℝ, E) is_closed_univ (λ x h, hU x) with
    ⟨ι, b, hb⟩,
  let ρ := b.to_smooth_partition_of_unity,
  have sum_ρ := λ x, ρ.sum_eq_one (mem_univ x),
  have nonneg_ρ := ρ.nonneg,
  have tsupp_rho : ∀ i, tsupport (ρ i) ⊆ U (b.c i) := hb.to_smooth_partition_of_unity,
  have lf : locally_finite (λ (i : ι), support (λ x, ρ i x • φ (b.c i) x)),
  { refine ρ.locally_finite.subset (λ i x hx hx', hx _),
    dsimp only,
    rw [hx', zero_smul] },
  refine ⟨λ x : E, (∑ᶠ i, (ρ i x) • φ (b.c i) x), cont_diff_iff_cont_diff_at.mpr _, _⟩,
  all_goals { intros x₀, rcases finsum.exists_finset lf x₀ with ⟨s, hs⟩  },
  { apply cont_diff_at.congr_of_eventually_eq _ hs,
    apply cont_diff_at.sum (λ i hi, _),
    by_cases hx₀ : x₀ ∈ U (b.c i),
    { apply cont_diff_at.smul,
      { exact ((ρ i).smooth.cont_diff.cont_diff_at).of_le le_top },
      { apply ((hφ $ b.c i).1 x₀ hx₀).cont_diff_at,
        apply (U_op $ b.c i).mem_nhds hx₀ } },
    { apply cont_diff_at_of_not_mem,
      dsimp only,
      intros Hx₀,
      have : x₀ ∉ tsupport (ρ i) := λ h, hx₀ (tsupp_rho i h),
      exact this (tsupport_smul (φ (b.c i)) (ρ i) Hx₀) } },
  { have := λ i, (hφ $ b.c i).2,
    rw show ∑ᶠ i, ρ i x₀ • φ (b.c i) x₀ = ∑ i in s, ρ i x₀ • φ (b.c i) x₀, from hs.eq_of_nhds,
    -- We don't know enough. We need to know that x₀ ∈ U (b.c i) for each i in s.
    sorry },
end

[Patrick Massot]

And I still wish I could do that on an open set, but mathlib doesn't seem to know that an open set in a real vector space is a manifold (at least type class search doesn't know).

[Oliver Nash]

Distantly-related PR #13006

[Heather Macbeth]

Patrick Massot said:

And I still wish I could do that on an open set, but mathlib doesn't seem to know that an open set in a real vector space is a manifold (at least type class search doesn't know).

@Patrick Massot docs#topological_space.opens.smooth_manifold_with_corners (I can't remember why I didn't make it an instance)

[Patrick Massot]

Update: I proved the lemma in the absolute case. I'll clean up and prove the open set case tomorrow.

[Yury G. Kudryashov]

My version of the "finset" lemma is in #13013

[Yury G. Kudryashov]

I use mul_support/support instead of tsupport because that's what I used in various lemmas about partition of unity that were written before tsupport was added to mathlib. We should have a lemma that relates locally_finite for these two families of sets.

[Yury G. Kudryashov]

docs#locally_finite.closure and docs#locally_finite.mono prove that they're equivalent. We should agree on the canonical form. Probably, tsupport is better because it is what people usually use in analysis.

[Yury G. Kudryashov]

I'm going to bed now. Probably, I won't have time for Lean till next evening (Toronto time).

[Patrick Massot]

The lemmas involving support are useful in algebra. The usefulness of the tsupport versions comes from docs#not_mem_closure_support_iff_eventually_eq

[Patrick Massot]

I cleaned up a bit my code and created more sorry about cont_mdiff. Now I need to stop and do real work (grading stuff and administration). I'd be grateful if someone among @Yury G. Kudryashov , @Sebastien Gouezel or @Heather Macbeth could do a quick review of https://github.com/leanprover-community/sphere-eversion/blob/master/src/to_mathlib/partition.lean. Note this file is completely independent from the sphere eversion project, so you can simply drop it into a recent mathlib.

[Patrick Massot]

@Floris van Doorn and @Oliver Nash may want to have a look as well

[Patrick Massot]

In particular I'd be grateful to learn that cont_mdiff_within_at.smul and cont_mdiff_within_at.add are actually already there somewhere.

[Patrick Massot]

Of course I hope I'll be able to get a version where the source is a manifold, and then apply it to open sets in vector spaces, using Heather's non-instance.

[Patrick Massot]

Heather Macbeth said:

Patrick Massot said:

And I still wish I could do that on an open set, but mathlib doesn't seem to know that an open set in a real vector space is a manifold (at least type class search doesn't know).

Patrick Massot docs#topological_space.opens.smooth_manifold_with_corners (I can't remember why I didn't make it an instance)

Acutally this seems to be instance. Since you know about this, could you try to prove a version of docs#cont_mdiff_iff_cont_diff relating cont_diff_on for an open set of a vector space with cont_mdiff for the manifold structure on the corresponding subtype?

[Heather Macbeth]

Sure, I'll try this afternoon.

[Patrick Massot]

Great! I think I'll need:

import geometry.manifold.partition_of_unity

noncomputable theory
universes uM uH

open_locale topological_space filter manifold
open filter topological_space function set

variables
  {E : Type*} [normed_group E] [normed_space ℝ E]
  {F : Type*} [normed_group F] [normed_space ℝ F]

lemma cont_mdiff_iff_cont_diff_on {s : opens E}  {f : E → F} {n : with_top ℕ} :
  cont_mdiff 𝓘(ℝ, E) 𝓘(ℝ, F) n (f ∘ (coe : s → E)) ↔ cont_diff_on ℝ n f s :=
sorry

lemma cont_mdiff_iff_cont_diff_on' {s : opens E} [decidable_pred (λ x, x ∈ s)]
  {f : s → F} {n : with_top ℕ} :
  cont_mdiff 𝓘(ℝ, E) 𝓘(ℝ, F) n f ↔ cont_diff_on ℝ n (λ x : E, if hx : x ∈ s then f ⟨x, hx⟩ else 0) s :=
sorry

lemma cont_mdiff_on_iff_cont_diff_on' {s : opens E} {t : set E} {f : E → F} {n : with_top ℕ} :
  cont_mdiff_on 𝓘(ℝ, E) 𝓘(ℝ, F) n (f ∘ (coe : s → E)) (coe ⁻¹' t) ↔ cont_diff_on ℝ n f (s ∩ t) :=
sorry

[Patrick Massot]

I hope these are true. I'm sure you can feel my subtype pain from these statements. This all comes from trying to deduce from the manifold library results that are purely about open sets in vector spaces (we only have smooth partitions of unity in the manifold context).

[Patrick Massot]

You can see this at https://github.com/leanprover-community/sphere-eversion/blob/2a042511a8f70f3917c914685418db6231e57110/src/to_mathlib/partition.lean#L356-L360

[Patrick Massot]

And I should also ping @Sebastien Gouezel

[Heather Macbeth]

@Patrick Massot I got as far as this translation:

import geometry.manifold.local_invariant_properties

open topological_space structure_groupoid.local_invariant_prop

variables {H : Type*} {M : Type*} [topological_space H] [topological_space M] [charted_space H M]
{H' : Type*} {M' : Type*} [topological_space H'] [topological_space M'] [charted_space H' M']

variables {G : structure_groupoid H} {G' : structure_groupoid H'}
{P : (H → H') → set H → H → Prop} (hG : G.local_invariant_prop G' P)

include hG

lemma cont_mdiff_iff_cont_mdiff_on {s : opens M}  {f : M → M'} :
  lift_prop P (f ∘ (coe : s → M)) ↔ lift_prop_on P f s :=
sorry

lemma cont_mdiff_iff_cont_diff_on' [inhabited M'] {s : opens M} [decidable_pred (λ x, x ∈ s)]
  {f : s → M'} :
  lift_prop P f ↔ lift_prop_on P (λ x : M, if hx : x ∈ s then f ⟨x, hx⟩ else default) s :=
sorry

lemma cont_mdiff_on_iff_cont_diff_on' {s : opens M} {t : set M} {f : M → M'} :
  lift_prop_on P (f ∘ (coe : s → M)) (coe ⁻¹' t) ↔ lift_prop_on P f (s ∩ t) :=
sorry

[Patrick Massot]

I don't understand what this means. Does it mean that if you can prove those lemmas then mine follow?

[Heather Macbeth]

Patrick Massot said:

I don't understand what this means. Does it mean that if you can prove those lemmas then mine follow?

Sorry for the slow reply. Yes, I claim that this is a suitable general context, and your lemmas should be 1-line specializations.

[Patrick Massot]

@Heather Macbeth I can confirm your lemmas imply mines.

[Patrick Massot]

Did you make any progress on proving your lemmas?