Energy Quantities

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballEnergy {n m : ℕ} (u : Domain n → Target m) (a : Domain n) (r : ℝ) : ℝ

Energy on a ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballRadialEnergy {n m : ℕ} (u : Domain n → Target m) (a : Domain n) (r : ℝ) : ℝ

Radial energy on a ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallEnergy {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (r : ℝ) : ℝ

Weak energy on a ball, written in terms of the chosen weak gradient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallRadialEnergy {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (r : ℝ) : ℝ

Weak radial energy on a ball, written in terms of the chosen weak gradient.

Equations

• One or more equations did not get rendered due to their size.

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

The open ball of radius 0 is empty, so its weak energy is zero.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallRadialEnergy_zero_radius {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) : weakBallRadialEnergy Du a 0 = 0

The open ball of radius 0 is empty, so its weak radial energy is zero.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor (n : ℕ) (r : ℝ) : ℝ

The factor r^(2-n) as an integer power.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor n r = r ^ (2 - ↑n)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor_continuousOn_Icc {n : ℕ} {s r : ℝ} (hs : 0 < s) : ContinuousOn (thetaFactor n) (Set.Icc s r)

The monotonicity factor is continuous on any closed interval bounded away from the origin.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.theta {n m : ℕ} (u : Domain n → Target m) (a : Domain n) (r : ℝ) : ℝ

The monotonicity quantity Theta_u(a,r).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (r : ℝ) : ℝ

Weak monotonicity quantity, using the weak gradient energy.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor_absolutelyContinuousOnInterval {n : ℕ} {s r : ℝ} (hs : 0 < s) (hsr : s < r) : AbsolutelyContinuousOnInterval (thetaFactor n) s r

The factor r^(2-n) is smooth, hence absolutely continuous, on every strictly positive radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.deriv_thetaFactor {n : ℕ} {rho : ℝ} : deriv (thetaFactor n) rho = (2 - ↑n) * rho ^ (1 - ↑n)

Derivative of the monotonicity weight.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor_boundary_algebra {n : ℕ} {rho E E' Q' : ℝ} (hrho : rho ≠ 0) (hboundary : rho * E' - (↑n - 2) * E = 2 * rho * Q') : deriv (thetaFactor n) rho * E + thetaFactor n rho * E' = 2 * thetaFactor n rho * Q'

Pointwise algebra turning the boundary identity into the derivative of the monotonicity quantity.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.annulusWeight (n : ℕ) (a x : Domain n) : ℝ

The annular weight |x-a|^(2-n).

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.annulusWeight n a x = ‖x - a‖ ^ (2 - ↑n)

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.monotonicityRhs {n m : ℕ} (u : Domain n → Target m) (a : Domain n) (s r : ℝ) : ℝ

Right-hand side of the monotonicity formula on B_r(a) \ B_s(a).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakMonotonicityRhs {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (s r : ℝ) : ℝ

Right-hand side of the weak monotonicity formula on B_r(a) \ B_s(a).

Equations

• One or more equations did not get rendered due to their size.

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

The weak annular radial-energy term is nonnegative.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff (n : ℕ) (phi : ℝ → ℝ) (x : Domain n) : ℝ

Coefficient multiplying the weak energy density in the radial identity.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff n phi x = (↑n - 2) * phi ‖x‖ + ‖x‖ * deriv phi ‖x‖

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff {n : ℕ} (phi : ℝ → ℝ) (x : Domain n) : ℝ

Coefficient multiplying the weak radial-energy density in the radial identity.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff phi x = ‖x‖ * deriv phi ‖x‖

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff_continuous {n : ℕ} {phi : ℝ → ℝ} (hphi : Continuous phi) (hdphi : Continuous (deriv phi)) : Continuous fun (x : Domain n) => weakRadialMainCoeff n phi x

Continuity of the main radial cutoff coefficient, assuming phi and phi' are continuous.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff_continuous {n : ℕ} {phi : ℝ → ℝ} (hdphi : Continuous (deriv phi)) : Continuous fun (x : Domain n) => weakRadialRhsCoeff phi x

Continuity of the radial-energy cutoff coefficient, assuming phi' is continuous.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff_continuous_of_contDiff {n : ℕ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : Continuous fun (x : Domain n) => weakRadialMainCoeff n phi x

A C¹ scalar cutoff gives a continuous main radial coefficient.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff_continuous_of_contDiff {n : ℕ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : Continuous fun (x : Domain n) => weakRadialRhsCoeff phi x

A C¹ scalar cutoff gives a continuous radial-energy coefficient.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff_aestronglyMeasurable {n : ℕ} {Ω : Set (Domain n)} {phi : ℝ → ℝ} (hphi : Continuous phi) (hdphi : Continuous (deriv phi)) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x) (MeasureTheory.volume.restrict Ω)

The main radial cutoff coefficient is a.e. strongly measurable on any set.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff_aestronglyMeasurable {n : ℕ} {Ω : Set (Domain n)} {phi : ℝ → ℝ} (hdphi : Continuous (deriv phi)) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω)

The radial-energy cutoff coefficient is a.e. strongly measurable on any set.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff_aestronglyMeasurable_of_contDiff {n : ℕ} {Ω : Set (Domain n)} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x) (MeasureTheory.volume.restrict Ω)

The main radial cutoff coefficient is a.e. strongly measurable for a C¹ scalar cutoff.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff_aestronglyMeasurable_of_contDiff {n : ℕ} {Ω : Set (Domain n)} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω)

The radial-energy cutoff coefficient is a.e. strongly measurable for a C¹ scalar cutoff.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainCoeff_ae_bound_on_ball_of_radius_bounds {n : ℕ} {phi : ℝ → ℝ} {R0 M0 M1 : ℝ} (hphi_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖phi t‖ ≤ M0) (hdphi_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv phi t‖ ≤ M1) (hR0_nonneg : 0 ≤ R0) : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialMainCoeff n phi x‖ ≤ ‖↑n - 2‖ * M0 + R0 * M1

If phi and phi' are bounded on [0, R0], then the main radial coefficient is a.e. bounded on B_R0(0).

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsCoeff_ae_bound_on_ball_of_radius_bound {n : ℕ} {phi : ℝ → ℝ} {R0 M1 : ℝ} (hdphi_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv phi t‖ ≤ M1) (hR0_nonneg : 0 ≤ R0) : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialRhsCoeff phi x‖ ≤ R0 * M1

If phi' is bounded on [0, R0], then the radial-energy coefficient is a.e. bounded on B_R0(0).