Local L² bridge

This module isolates the measure-theoretic L²_loc input used by the Sobolev bridge. The map and gradient components are phrased using mathlib's MemLp on compact restrictions. For the gradient we also keep the global a.e. measurability field explicitly: local compact MemLp data is enough for the energy integrability part, while global a.e. measurability on an arbitrary domain is a separate measurable-cover problem.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocallyMemLpTwoIn {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] (f : Domain n → E) (Ω : Set (Domain n)) : Prop

Local L² membership via mathlib's MemLp, tested on every compact subset of the domain.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.locallyMemLpTwoIn_to_locallyIntegrable_norm_sq {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : Domain n → E} {Ω : Set (Domain n)} (hf : LocallyMemLpTwoIn f Ω) : LocallyIntegrableScalarIn (fun (x : Domain n) => ‖f x‖ ^ 2) Ω

Local MemLp 2 implies local integrability of the squared norm.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.mapLocallyL2In_of_locallyMemLpTwoIn {n m : ℕ} {u : Domain n → Target m} {Ω : Set (Domain n)} (hu : LocallyMemLpTwoIn u Ω) : MapLocallyL2In u Ω

Local MemLp 2 for the map gives the custom map L²_loc field.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.GradientLocallyMemLpTwoIn {n m : ℕ} (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

Local gradient L² membership via mathlib's MemLp, together with global a.e. strong measurability on the domain.

• aestronglyMeasurable : GradientAEStronglyMeasurableIn Du Ω
• memLpTwo_loc : LocallyMemLpTwoIn Du Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientLocallyL2In_of_gradientLocallyMemLpTwoIn {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (hDu : GradientLocallyMemLpTwoIn Du Ω) : GradientLocallyL2In Du Ω

Local MemLp 2 for the gradient field gives integrability of the Hilbert-Schmidt energy density on compact subsets.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.GradientLocallyMemLpTwoIn.toGradientAEStronglyMeasurableIn {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (hDu : GradientLocallyMemLpTwoIn Du Ω) : GradientAEStronglyMeasurableIn Du Ω

The a.e. measurability component of the gradient local MemLp 2 package.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocalL2DataIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

The local L² data needed before adding the weak-gradient relation.

• map_memLpTwo_loc : LocallyMemLpTwoIn u Ω
• gradient_memLpTwo_loc : GradientLocallyMemLpTwoIn Du Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocalL2DataIn.toMapLocallyL2In {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : LocalL2DataIn u Du Ω) : MapLocallyL2In u Ω

Extract the custom map L²_loc field from local MemLp 2 data.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocalL2DataIn.toGradientAEStronglyMeasurableIn {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : LocalL2DataIn u Du Ω) : GradientAEStronglyMeasurableIn Du Ω

Extract the custom gradient a.e. measurability field from local gradient MemLp 2 data.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocalL2DataIn.toGradientLocallyL2In {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : LocalL2DataIn u Du Ω) : GradientLocallyL2In Du Ω

Extract the custom gradient L²_loc field from local gradient MemLp 2 data.