RellichKondrachov.Geometry.Manifold.Sobolev.ChartData

Chart/partition-of-unity data for defining Sobolev spaces on compact manifolds.

For the Laplace–Beltrami compact-resolvent discharge (lean-103.5.2.26), we ultimately need Sobolev spaces H¹, H² on a compact smooth manifold M together with continuous maps to L² and to suitable “derivative” targets.

At the current Mathlib pin, the most robust starting point is to make the analytic definitions relative to explicit finite chart data and a smooth partition of unity subordinate to those charts; later work can address atlas-independence.

This file provides:

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData: a finite family of chart centers together with a subordinate SmoothPartitionOfUnity.
• RellichKondrachov.Geometry.Manifold.Sobolev.exists_finiteChartData_chartAt: on a compact smooth manifold, there exists such data subordinate to chartAt sources.

structure RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] (H : Type u_1) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] : Type (max u_2 (u_3 + 1))

Finite chart centers with a smooth partition of unity subordinate to chartAt sources.

• ι : Type u_3

  An index type for the chart data.

• instFintype : Fintype self.ι

  The index type is finite.

• center : self.ι → M

  The chosen chart centers.

• ρ : SmoothPartitionOfUnity self.ι I M

  A smooth partition of unity indexed by ι on M.

• subordinate : self.ρ.IsSubordinate fun (i : self.ι) => (chartAt H (self.center i)).source

  Subordination to the chart domains: closure (support (ρ i)) ⊆ (chartAt H (center i)).source.

@[simp]

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.subordinate_apply {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] (d : FiniteChartData H M I) (i : d.ι) : closure (Function.support ⇑(d.ρ i)) ⊆ (chartAt H (d.center i)).source

theorem RellichKondrachov.Geometry.Manifold.Sobolev.exists_finiteChartData_chartAt {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [T2Space M] [CompactSpace M] : Nonempty (FiniteChartData H M I)

On a compact smooth manifold, there exists finite chart data subordinate to chartAt sources.