Radius Weights

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn (R0 : ℝ) (c : ℝ → ℝ) : Prop

The class of radius weights we actually need in the weak monotonicity argument: measurable on (0, R0) and essentially bounded there. The earlier unrestricted formulas with ∀ c : ℝ → ℝ are convenient wrappers, but this is the realistic target for a direct measure-theoretic coarea proof.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.aestronglyMeasurable {R0 : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) : MeasureTheory.AEStronglyMeasurable c (radiusIntervalMeasure R0)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.exists_ae_bound {R0 : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (rho : ℝ) ∂radiusIntervalMeasure R0, ‖c rho‖ ≤ C

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_of_aestronglyMeasurable_ae_bound {R0 : ℝ} {c : ℝ → ℝ} (hc_meas : MeasureTheory.AEStronglyMeasurable c (radiusIntervalMeasure R0)) (hc_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (rho : ℝ) ∂radiusIntervalMeasure R0, ‖c rho‖ ≤ C) : RadiusWeightOn R0 c

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_of_aestronglyMeasurable_bound_on_Ioo {R0 : ℝ} {c : ℝ → ℝ} {C : ℝ} (hc_meas : MeasureTheory.AEStronglyMeasurable c (radiusIntervalMeasure R0)) (hC_nonneg : 0 ≤ C) (hC : ∀ rho ∈ Set.Ioo 0 R0, ‖c rho‖ ≤ C) : RadiusWeightOn R0 c

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_const (R0 k : ℝ) : RadiusWeightOn R0 fun (x : ℝ) => k

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.indicator {R0 : ℝ} {c : ℝ → ℝ} {s : Set ℝ} (hc : RadiusWeightOn R0 c) (hs : MeasurableSet s) : RadiusWeightOn R0 (s.indicator c)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_indicator_of_aestronglyMeasurable_bound_on_set {R0 : ℝ} {c : ℝ → ℝ} {s : Set ℝ} {C : ℝ} (hc_meas : MeasureTheory.AEStronglyMeasurable (s.indicator c) (radiusIntervalMeasure R0)) (hC_nonneg : 0 ≤ C) (hC : ∀ rho ∈ s, ‖c rho‖ ≤ C) : RadiusWeightOn R0 (s.indicator c)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_indicator_const {R0 a b k : ℝ} : RadiusWeightOn R0 ((Set.Ioo a b).indicator fun (x : ℝ) => k)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_indicator_one {R0 a b : ℝ} : RadiusWeightOn R0 ((Set.Ioo a b).indicator fun (x : ℝ) => 1)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.add {R0 : ℝ} {c d : ℝ → ℝ} (hc : RadiusWeightOn R0 c) (hd : RadiusWeightOn R0 d) : RadiusWeightOn R0 fun (rho : ℝ) => c rho + d rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_finset_sum_indicator_const_Ioo {R0 : ℝ} {ι : Type u_1} (s : Finset ι) (a b k : ι → ℝ) : RadiusWeightOn R0 fun (rho : ℝ) => ∑ i ∈ s, (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) rho

Finite linear combinations of interval-indicator constants are admissible radius weights.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApprox (R0 : ℝ) (c : ℝ → ℝ) : Prop

Pointwise finite interval-step approximation by uniformly bounded radius weights. This is the concrete approximation package needed to pass the finite-interval formula to a limiting radius weight by dominated convergence.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApproxAE (R0 : ℝ) (c : ℝ → ℝ) : Prop

The practically useful version of finite interval-step approximation: convergence is required on (0, R0) away from a countable set of bad radii. This matches the grid-partition approximations used for continuous weights, where all possible partition boundaries form a countable exceptional set.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApprox.toAE {R0 : ℝ} {c : ℝ → ℝ} (h : RadiusWeightFiniteIntervalStepApprox R0 c) : RadiusWeightFiniteIntervalStepApproxAE R0 c

A pointwise finite interval-step approximation is, in particular, an a.e.-valid approximation with empty exceptional set.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightFiniteIntervalStepApprox_finset_sum_indicator_const_Ioo {R0 : ℝ} {s : Finset ℕ} {a b k : ℕ → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hab : ∀ i ∈ s, a i ≤ b i) (hb : ∀ i ∈ s, b i ≤ R0) : RadiusWeightFiniteIntervalStepApprox R0 fun (rho : ℝ) => ∑ i ∈ s, (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) rho

A finite interval-step weight is realized by the constant approximation sequence.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightFiniteIntervalStepApproxAE_const {R0 r : ℝ} (hR0_nonneg : 0 ≤ R0) : RadiusWeightFiniteIntervalStepApproxAE R0 fun (x : ℝ) => r

Constant radius weights are approximable on (0, R0) by the single interval (0, R0).

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApproxAE.add {R0 : ℝ} {c d : ℝ → ℝ} (hc : RadiusWeightFiniteIntervalStepApproxAE R0 c) (hd : RadiusWeightFiniteIntervalStepApproxAE R0 d) : RadiusWeightFiniteIntervalStepApproxAE R0 fun (rho : ℝ) => c rho + d rho

Finite interval-step approximability is closed under addition. The proof encodes the two finite index sets into the even and odd natural numbers.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApproxAE.const_mul {R0 r : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightFiniteIntervalStepApproxAE R0 c) : RadiusWeightFiniteIntervalStepApproxAE R0 fun (rho : ℝ) => r * c rho

Finite interval-step approximability is closed under multiplication by a constant.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApproxAE.neg {R0 : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightFiniteIntervalStepApproxAE R0 c) : RadiusWeightFiniteIntervalStepApproxAE R0 fun (rho : ℝ) => -c rho

Finite interval-step approximability is closed under negation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightFiniteIntervalStepApproxAE.sub {R0 : ℝ} {c d : ℝ → ℝ} (hc : RadiusWeightFiniteIntervalStepApproxAE R0 c) (hd : RadiusWeightFiniteIntervalStepApproxAE R0 d) : RadiusWeightFiniteIntervalStepApproxAE R0 fun (rho : ℝ) => c rho - d rho

Finite interval-step approximability is closed under subtraction.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.neg {R0 : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) : RadiusWeightOn R0 fun (rho : ℝ) => -c rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.sub {R0 : ℝ} {c d : ℝ → ℝ} (hc : RadiusWeightOn R0 c) (hd : RadiusWeightOn R0 d) : RadiusWeightOn R0 fun (rho : ℝ) => c rho - d rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.mul {R0 : ℝ} {c d : ℝ → ℝ} (hc : RadiusWeightOn R0 c) (hd : RadiusWeightOn R0 d) : RadiusWeightOn R0 fun (rho : ℝ) => c rho * d rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.const_mul {R0 k : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) : RadiusWeightOn R0 fun (rho : ℝ) => k * c rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.mul_const {R0 k : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) : RadiusWeightOn R0 fun (rho : ℝ) => c rho * k

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_id (R0 : ℝ) : RadiusWeightOn R0 fun (rho : ℝ) => rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_of_contDiff_one {R0 : ℝ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : RadiusWeightOn R0 phi

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_deriv_of_contDiff_one {R0 : ℝ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : RadiusWeightOn R0 (deriv phi)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_rho_mul_deriv_of_contDiff_one {R0 : ℝ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : RadiusWeightOn R0 fun (rho : ℝ) => rho * deriv phi rho

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_radialMainCoeff_of_contDiff_one {n : ℕ} {R0 : ℝ} {phi : ℝ → ℝ} (hphi : ContDiff ℝ 1 phi) : RadiusWeightOn R0 fun (rho : ℝ) => (↑n - 2) * phi rho + rho * deriv phi rho