Radial cutoff packages

This module packages the scalar radial cutoffs used to test weak stationarity. It is deliberately independent of the later radial integral identities.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.AdmissibleRadialCutoff (n : ℕ) (R0 M0 M1 : ℝ) (phi : ℝ → ℝ) : Prop

The precise cutoff interface needed by the weak radial identity on B_R0(0).

Concrete cutoff families, such as the smooth approximations of sharp radial annuli used later in the monotonicity proof, should be proved to satisfy this structure. Keeping the interface explicit prevents the downstream weak identity from depending on the implementation details of a particular cutoff.

• radius_nonneg : 0 ≤ R0
• differentiable : Differentiable ℝ phi
• contDiff : ContDiff ℝ 1 phi
• vectorField_contDiff : ContDiff ℝ 1 (radialVectorField phi)
• vectorField_hasCompactSupport : HasCompactSupport (radialVectorField phi)
• vectorField_support_subset : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0
• phi_bound (t : ℝ) : 0 ≤ t → t ≤ R0 → ‖phi t‖ ≤ M0
• deriv_bound (t : ℝ) : 0 ≤ t → t ≤ R0 → ‖deriv phi t‖ ≤ M1

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.norm_mem_tsupport_of_mem_radialVectorField_tsupport {n : ℕ} {phi : ℝ → ℝ} {x : Domain n} (hx : x ∈ tsupport (radialVectorField phi)) : ‖x‖ ∈ tsupport phi

If a point lies in the topological support of x ↦ phi(|x|) x, then its radius lies in the topological support of phi.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_tsupport_subset_closedBall_of_scalar_tsupport {n : ℕ} {phi : ℝ → ℝ} {R : ℝ} (hphi : tsupport phi ⊆ Metric.closedBall 0 R) : tsupport (radialVectorField phi) ⊆ Metric.closedBall 0 R

If a scalar radial coefficient is topologically supported in [-R, R], then the vector field x ↦ phi(|x|) x is topologically supported in closedBall 0 R.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_tsupport_subset_ball_of_scalar_tsupport_Iio {n : ℕ} {phi : ℝ → ℝ} {R0 : ℝ} (hphi : tsupport phi ⊆ Set.Iio R0) : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0

If the scalar coefficient is supported in (-∞, R0), then the radial vector field is supported in the ball B_R0(0). This is the support statement needed for sharp cutoffs that are allowed to be nonzero near the origin.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_hasCompactSupport_of_scalar_tsupport_Iio {n : ℕ} {phi : ℝ → ℝ} {R0 : ℝ} (hphi : tsupport phi ⊆ Set.Iio R0) : HasCompactSupport (radialVectorField phi)

The same support assumption gives compact support of the radial vector field, because it is contained in the closed ball of radius R0.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_tsupport_subset_closedBall_of_contDiffBump {n : ℕ} (f : ContDiffBump 0) : tsupport (radialVectorField fun (t : ℝ) => ↑f t) ⊆ Metric.closedBall 0 f.rOut

A one-dimensional ContDiffBump controls the support of its radial vector field by the outer radius of the bump.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_hasCompactSupport_of_contDiffBump {n : ℕ} (f : ContDiffBump 0) : HasCompactSupport (radialVectorField fun (t : ℝ) => ↑f t)

Compact support of the radial vector field generated by a one-dimensional ContDiffBump.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_tsupport_subset_ball_of_contDiffBump {n : ℕ} {R0 : ℝ} (f : ContDiffBump 0) (hRout : f.rOut < R0) : tsupport (radialVectorField fun (t : ℝ) => ↑f t) ⊆ Metric.ball 0 R0

A one-dimensional ContDiffBump whose outer radius is strictly below R0 has radial vector-field support inside B_R0(0).

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ContDiffBump.exists_deriv_bound_on_Icc (f : ContDiffBump 0) (R0 : ℝ) : ∃ (M1 : ℝ), ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv (fun (s : ℝ) => ↑f s) t‖ ≤ M1

The derivative of a one-dimensional ContDiffBump is bounded on every closed interval [0, R0]. We keep the bound existential because the later integrability arguments only need some finite constant.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_contDiff_of_contDiff_const_near_origin {n : ℕ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) (hconst : ∃ (ε : ℝ), 0 < ε ∧ ∀ (t : ℝ), |t| < ε → phi t = phi 0) : ContDiff ℝ 1 (radialVectorField phi)

A C¹ scalar cutoff that is constant near the origin generates a C¹ radial vector field. Away from the origin this is the chain rule for the norm; at the origin the vector field is locally the linear map x ↦ phi 0 • x.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_norm_bound_on_Icc_of_continuous {f : ℝ → ℝ} (hf : Continuous f) (a b : ℝ) : ∃ (M : ℝ), ∀ (t : ℝ), a ≤ t → t ≤ b → ‖f t‖ ≤ M

A continuous real-valued function is bounded on a compact interval. The existential bound is the format needed by the cutoff integrability interface.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_deriv_bound_on_Icc_of_contDiff {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) (R0 : ℝ) : ∃ (M1 : ℝ), ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv phi t‖ ≤ M1

A C¹ real cutoff has bounded derivative on every compact interval.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.ConstNearOrigin (phi : ℝ → ℝ) : Prop

A scalar cutoff is constant in a symmetric neighborhood of the origin. This is the exact local regularity needed to make x ↦ phi ‖x‖ • x differentiable at the origin without proving the full general radial-extension theorem.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.ConstNearOrigin phi = ∃ (ε : ℝ), 0 < ε ∧ ∀ (t : ℝ), |t| < ε → phi t = phi 0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_admissibleRadialCutoff_of_contDiff_const_near_origin {n : ℕ} {R0 : ℝ} {phi : ℝ → ℝ} (hR0_nonneg : 0 ≤ R0) (hphi_diff : Differentiable ℝ phi) (hphi_cont : ContDiff ℝ 1 phi) (_hphi_compact : HasCompactSupport phi) (hphi_support : tsupport phi ⊆ Set.Iio R0) (hconst : ConstNearOrigin phi) : ∃ (M0 : ℝ) (M1 : ℝ), AdmissibleRadialCutoff n R0 M0 M1 phi

A scalar C¹ cutoff supported before R0 and flat near the origin gives the packaged admissible radial cutoff used by the weak stationarity argument.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_admissibleRadialCutoff_of_contDiff_and_vectorFieldContDiff {n : ℕ} {R0 : ℝ} {phi : ℝ → ℝ} (hR0_nonneg : 0 ≤ R0) (hphi_diff : Differentiable ℝ phi) (hphi_cont : ContDiff ℝ 1 phi) (_hphi_compact : HasCompactSupport phi) (hphi_support : tsupport phi ⊆ Set.Iio R0) (hX_cont : ContDiff ℝ 1 (radialVectorField phi)) : ∃ (M0 : ℝ) (M1 : ℝ), AdmissibleRadialCutoff n R0 M0 M1 phi

A scalar C¹ cutoff supported before R0 gives the packaged admissible radial cutoff once the C¹ regularity of its radial vector field is supplied directly. This is the correct replacement for the too-strong global flat-at-origin assumption.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.contDiff_one_intervalPrimitive_left {g : ℝ → ℝ} (hg : Continuous g) (b : ℝ) : ContDiff ℝ 1 fun (t : ℝ) => ∫ (x : ℝ) in t..b, g x

The interval primitive t ↦ ∫ x in t..b, g x is C¹ when g is continuous.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_tsupport_subset_Iio_lt_of_hasCompactSupport {g : ℝ → ℝ} {R0 : ℝ} (hg_compact : HasCompactSupport g) (hg_support : tsupport g ⊆ Set.Iio R0) : ∃ (U : ℝ), tsupport g ⊆ Set.Iio U ∧ U < R0

If a compactly supported real function has topological support contained in (-∞, R0), then the support is contained in (-∞, U) for some U < R0.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.exists_pos_lt_tsupport_subset_Ioi_of_hasCompactSupport {g : ℝ → ℝ} {R0 : ℝ} (hg_compact : HasCompactSupport g) (hg_support : tsupport g ⊆ Set.Ioo 0 R0) : ∃ (L : ℝ), 0 < L ∧ tsupport g ⊆ Set.Ioi L

If a compactly supported real function has topological support contained in (0, R0), then the support is contained in (L, ∞) for some 0 < L.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.intervalPrimitive_eq_zero_of_tsupport_subset_Iio {g : ℝ → ℝ} {U t b : ℝ} (hg_support : tsupport g ⊆ Set.Iio U) (ht : U < t) (hb : U < b) : ∫ (x : ℝ) in t..b, g x = 0

If the support of g lies to the left of U, then its interval primitive vanishes on intervals whose endpoints are both to the right of U.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.intervalPrimitive_eq_zero_of_tsupport_subset_Ioi {g : ℝ → ℝ} {L t b : ℝ} (hg_support : tsupport g ⊆ Set.Ioi L) (ht : t < L) (hb : b < L) : ∫ (x : ℝ) in t..b, g x = 0

If the support of g lies to the right of L, then its interval integral vanishes on intervals whose endpoints are both to the left of L.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.intervalPrimitive_eq_intervalPrimitive_zero_of_tsupport_subset_Ioi {g : ℝ → ℝ} {L t b : ℝ} (hg_cont : Continuous g) (hg_support : tsupport g ⊆ Set.Ioi L) (hL_pos : 0 < L) (ht : t < L) : ∫ (x : ℝ) in t..b, g x = ∫ (x : ℝ) in 0..b, g x

If the support of g is separated from the origin on the right, then the left interval primitive t ↦ ∫ x in t..b, g x is constant near the origin.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField_contDiff_of_contDiffBump {n : ℕ} (f : ContDiffBump 0) : ContDiff ℝ 1 (radialVectorField fun (t : ℝ) => ↑f t)

The radial vector field generated by a one-dimensional ContDiffBump is C¹. Away from the origin this is the usual chain rule for the norm; near the origin the bump is identically 1, so the vector field is locally the identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ContDiffBump.admissibleRadialCutoff {n : ℕ} {R0 M1 : ℝ} (f : ContDiffBump 0) (hRout : f.rOut < R0) (hderiv_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv (fun (s : ℝ) => ↑f s) t‖ ≤ M1) : AdmissibleRadialCutoff n R0 1 M1 fun (t : ℝ) => ↑f t

Build the admissible-cutoff package from a one-dimensional ContDiffBump, once the derivative bound on [0, R0] is supplied.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ContDiffBump.exists_admissibleRadialCutoff {n : ℕ} {R0 : ℝ} (f : ContDiffBump 0) (hRout : f.rOut < R0) : ∃ (M1 : ℝ), AdmissibleRadialCutoff n R0 1 M1 fun (t : ℝ) => ↑f t

A one-dimensional ContDiffBump whose outer radius is below R0 gives an admissible radial cutoff for some derivative-bound constant M1.