Center translations

This module starts the passage from the origin-centered theorem to arbitrary centers by isolating the translation identities needed for weakTheta.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateScalar {n : ℕ} (a : Domain n) (f : Domain n → ℝ) : Domain n → ℝ

Translate a scalar field by a domain point.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateScalar a f x = f (a + x)

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateGradient {n m : ℕ} (a : Domain n) (Du : Domain n → Gradient n m) : Domain n → Gradient n m

Translate a weak gradient field by a domain point.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateGradient a Du x = Du (a + x)

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.centeredDomain {n : ℕ} (a : Domain n) (Ω : Set (Domain n)) : Set (Domain n)

Translate a domain set to coordinates centered at a.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.centeredDomain a Ω = {x : LeanStationaryHarmonicMaps.StationaryHarmonicMap.Domain n | a + x ∈ Ω}

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateVectorFieldToOriginal {n : ℕ} (a : Domain n) (X : Domain n → Domain n) : Domain n → Domain n

Move a test vector field from coordinates centered at a back to the original coordinates.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateVectorFieldToOriginal a X y = X (y - a)

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateTargetTestToOriginal {n m : ℕ} (a : Domain n) (ψ : Domain n → Target m) : Domain n → Target m

Move a target-valued test map from coordinates centered at a back to the original coordinates.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.translateTargetTestToOriginal a ψ y = ψ (y - a)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.fderiv_translateVectorFieldToOriginal_add {n : ℕ} (X : Domain n → Domain n) (a x : Domain n) : fderiv ℝ (translateVectorFieldToOriginal a X) (a + x) = fderiv ℝ X x

The Fréchet derivative of a translated test vector field is the translated Fréchet derivative.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative_translateVectorFieldToOriginal_add {n : ℕ} (X : Domain n → Domain n) (a x : Domain n) (i : Fin n) : partialDerivative (translateVectorFieldToOriginal a X) i (a + x) = partialDerivative X i x

Coordinate derivatives are unchanged after translating a test vector field back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.fderiv_translateTargetTestToOriginal_add {n m : ℕ} (ψ : Domain n → Target m) (a x : Domain n) : fderiv ℝ (translateTargetTestToOriginal a ψ) (a + x) = fderiv ℝ ψ x

The Fréchet derivative of a translated target-valued test map is the translated Fréchet derivative.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative_translateTargetTestToOriginal_add {n m : ℕ} (ψ : Domain n → Target m) (a x : Domain n) (i : Fin n) : partialDerivative (translateTargetTestToOriginal a ψ) i (a + x) = partialDerivative ψ i x

Coordinate derivatives of target-valued test maps are unchanged after translating them back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.vectorFieldPartial_translateVectorFieldToOriginal_add {n : ℕ} (X : Domain n → Domain n) (a x : Domain n) (i j : Fin n) : vectorFieldPartial (translateVectorFieldToOriginal a X) i j (a + x) = vectorFieldPartial X i j x

Componentwise vector-field derivatives are unchanged after translating a test vector field back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.divergence_translateVectorFieldToOriginal_add {n : ℕ} (X : Domain n → Domain n) (a x : Domain n) : divergence (translateVectorFieldToOriginal a X) (a + x) = divergence X x

Divergence is unchanged after translating a test vector field back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationarityIntegrand_translateGradient_add {n m : ℕ} (Du : Domain n → Gradient n m) (X : Domain n → Domain n) (a x : Domain n) : weakStationarityIntegrand Du (translateVectorFieldToOriginal a X) (a + x) = weakStationarityIntegrand (translateGradient a Du) X x

The weak stationarity integrand is compatible with recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.contDiff_translateVectorFieldToOriginal {n : ℕ} {X : Domain n → Domain n} {a : Domain n} (hX : ContDiff ℝ 1 X) : ContDiff ℝ 1 (translateVectorFieldToOriginal a X)

Smoothness of compactly supported test vector fields is preserved when moving them from centered coordinates back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.hasCompactSupport_translateVectorFieldToOriginal {n : ℕ} {X : Domain n → Domain n} {a : Domain n} (hX : HasCompactSupport X) : HasCompactSupport (translateVectorFieldToOriginal a X)

Compact support is preserved when moving a test vector field from centered coordinates back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.tsupport_translateVectorFieldToOriginal {n : ℕ} (X : Domain n → Domain n) (a : Domain n) : tsupport (translateVectorFieldToOriginal a X) = (fun (y : Domain n) => y - a) ⁻¹' tsupport X

The topological support of a translated-back test field is the preimage of the original topological support under y ↦ y - a.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.contDiff_translateTargetTestToOriginal {n m : ℕ} {ψ : Domain n → Target m} {a : Domain n} (hψ : ContDiff ℝ 1 ψ) : ContDiff ℝ 1 (translateTargetTestToOriginal a ψ)

Smoothness of target-valued test maps is preserved when moving them from centered coordinates back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.hasCompactSupport_translateTargetTestToOriginal {n m : ℕ} {ψ : Domain n → Target m} {a : Domain n} (hψ : HasCompactSupport ψ) : HasCompactSupport (translateTargetTestToOriginal a ψ)

Compact support is preserved when moving a target-valued test map from centered coordinates back to the original coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.tsupport_translateTargetTestToOriginal {n m : ℕ} (ψ : Domain n → Target m) (a : Domain n) : tsupport (translateTargetTestToOriginal a ψ) = (fun (y : Domain n) => y - a) ⁻¹' tsupport ψ

The topological support of a translated-back target-valued test map is the preimage of the original topological support under y ↦ y - a.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.measurePreserving_add_left_volume {n : ℕ} (a : Domain n) : MeasureTheory.MeasurePreserving (fun (x : Domain n) => a + x) MeasureTheory.volume MeasureTheory.volume

Left translation preserves Lebesgue measure on the domain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.measurableEmbedding_add_left {n : ℕ} (a : Domain n) : MeasurableEmbedding fun (x : Domain n) => a + x

Left translation is a measurable embedding.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.integral_comp_add_right_volume {n : ℕ} (f : Domain n → ℝ) (a : Domain n) : ∫ (x : Domain n), f (x + a) = ∫ (x : Domain n), f x

Full-space Lebesgue integration is invariant under right translation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.integral_comp_add_left_volume {n : ℕ} (f : Domain n → ℝ) (a : Domain n) : ∫ (x : Domain n), f (a + x) = ∫ (x : Domain n), f x

Full-space Lebesgue integration is invariant under left translation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.setIntegral_preimage_add_left_eq {n : ℕ} (f : Domain n → ℝ) (a : Domain n) {s : Set (Domain n)} (hs : MeasurableSet s) : ∫ (x : Domain n) in (fun (x : Domain n) => a + x) ⁻¹' s, f (a + x) = ∫ (x : Domain n) in s, f x

Set integrals are invariant under the change of variables x ↦ a + x.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationaryIn_centeredDomain {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hstationary : WeakStationaryIn Du Ω) (hΩ_meas : MeasurableSet Ω) : WeakStationaryIn (translateGradient a Du) (centeredDomain a Ω)

Weak stationarity is preserved by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.hasWeakGradientIn_centeredDomain {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hweak : HasWeakGradientIn u Du Ω) (hΩ_meas : MeasurableSet Ω) : HasWeakGradientIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)

The weak-gradient integration-by-parts relation is preserved by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.preimage_add_left_ball_center {n : ℕ} (a : Domain n) (r : ℝ) : (fun (x : Domain n) => a + x) ⁻¹' Metric.ball a r = Metric.ball 0 r

The preimage of a ball centered at a under x ↦ a + x is the origin-centered ball of the same radius.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.preimage_add_left_closedBall_center {n : ℕ} (a : Domain n) (r : ℝ) : (fun (x : Domain n) => a + x) ⁻¹' Metric.closedBall a r = Metric.closedBall 0 r

The preimage of a closed ball centered at a under x ↦ a + x is the origin-centered closed ball of the same radius.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.measurableSet_centeredDomain {n : ℕ} {a : Domain n} {Ω : Set (Domain n)} (hΩ : MeasurableSet Ω) : MeasurableSet (centeredDomain a Ω)

Measurability of a domain is preserved when recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.closedBall_subset_centeredDomain_of_closedBall_subset {n : ℕ} {a : Domain n} {Ω : Set (Domain n)} {R0 : ℝ} (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) : Metric.closedBall 0 R0 ⊆ centeredDomain a Ω

A closed ball contained in Ω becomes an origin-centered closed ball contained in the recentered domain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.locallyIntegrableScalarIn_centeredDomain {n : ℕ} {f : Domain n → ℝ} {Ω : Set (Domain n)} {a : Domain n} (hf : LocallyIntegrableScalarIn f Ω) : LocallyIntegrableScalarIn (translateScalar a f) (centeredDomain a Ω)

Local scalar integrability is preserved by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.mapLocallyL2In_centeredDomain {n m : ℕ} {u : Domain n → Target m} {Ω : Set (Domain n)} {a : Domain n} (hu : MapLocallyL2In u Ω) : MapLocallyL2In (fun (x : Domain n) => u (a + x)) (centeredDomain a Ω)

The L²_loc map part of W^{1,2}_{loc} is preserved by recentering.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientLocallyL2In_centeredDomain {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hgrad : GradientLocallyL2In Du Ω) : GradientLocallyL2In (translateGradient a Du) (centeredDomain a Ω)

The L²_loc gradient-energy part of W^{1,2}_{loc} is preserved by recentering.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientAEStronglyMeasurableIn_centeredDomain {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hDu : GradientAEStronglyMeasurableIn Du Ω) : GradientAEStronglyMeasurableIn (translateGradient a Du) (centeredDomain a Ω)

A.e. strong measurability of the weak gradient is preserved by recentering.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.w12LocIn_centeredDomain {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hmap : W12LocIn u Du Ω) (hΩ_meas : MeasurableSet Ω) : W12LocIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)

The concrete W^{1,2}_{loc} package is preserved by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationaryMapIn_centeredDomain {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) : WeakStationaryMapIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)

The full weak stationary map package is preserved by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallEnergy_translateGradient_zero {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (r : ℝ) : weakBallEnergy (translateGradient a Du) 0 r = weakBallEnergy Du a r

The weak ball energy centered at a is the origin-centered energy of the translated gradient field.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_translateGradient_zero {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (r : ℝ) : weakTheta (translateGradient a Du) 0 r = weakTheta Du a r

The weak monotonicity quantity is unchanged after recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialDerivative_translateGradient_zero {n m : ℕ} (Du : Domain n → Gradient n m) (a x : Domain n) : weakRadialDerivative (translateGradient a Du) 0 x = weakRadialDerivative Du a (a + x)

The weak radial derivative is unchanged by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_translateGradient_zero {n m : ℕ} (Du : Domain n → Gradient n m) (a x : Domain n) : weakRadialEnergyDensity (translateGradient a Du) 0 x = weakRadialEnergyDensity Du a (a + x)

The weak radial-energy density is unchanged by recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakMonotonicityRhs_translateGradient_zero {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (s r : ℝ) : weakMonotonicityRhs (translateGradient a Du) 0 s r = weakMonotonicityRhs Du a s r

The annular right-hand side in the weak monotonicity formula is unchanged after recentering coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_centered_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap_centered : WeakStationaryMapIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) : MonotoneOn (weakTheta Du a) (Set.Ioo 0 R0)

Arbitrary-center Euclidean weak monotonicity, reduced to the origin-centered theorem for the translated map and translated weak gradient.