Exact source: MathlibAnnex/MeasureTheory/Integral/MaximalMinorBoundary.lean
Pinned GitHub source · Raw UTF-8 source
Back to Boundary agreement determines maximal-minor integrals
1import MathlibAnnex.MeasureTheory.Integral.MaximalMinor2import Mathlib.Analysis.Convex.Gauge3import Mathlib.Analysis.Convex.Measure45/-!6# Pointwise boundary agreement and maximal-minor integrals78The public theorem applies to any continuous seminorm whose closed unit ball9is compact. Boundary equality is pointwise on the seminorm unit sphere.10-/11noncomputable section12open Set Function MeasureTheory Filter13open scoped BigOperators Topology NNReal14namespace MathlibAnnex15namespace NullLagrangian1617private structure SeminormBall (n : ℕ) where18 p : Seminorm ℝ (Fin n → ℝ)19 continuous_p : Continuous p20 isCompact_closedBall : IsCompact (p.closedBall 0 1)2122namespace SeminormBall23private def unitBall {n : ℕ} (M : SeminormBall n) : Set (Fin n → ℝ) := M.p.closedBall 0 124@[simp] private theorem mem_unitBall {n : ℕ} (M : SeminormBall n) {x : Fin n → ℝ} :25 x ∈ M.unitBall ↔ M.p x ≤ 1 := by simp [unitBall]26private theorem isCompact_unitBall {n : ℕ} (M : SeminormBall n) : IsCompact M.unitBall := M.isCompact_closedBall27private theorem isClosed_unitBall {n : ℕ} (M : SeminormBall n) : IsClosed M.unitBall := M.isCompact_unitBall.isClosed28private theorem measurableSet_unitBall {n : ℕ} (M : SeminormBall n) : MeasurableSet M.unitBall := M.isClosed_unitBall.measurableSet29end SeminormBall30private abbrev Lipschitz {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) :=31 ∃ C : ℝ≥0, LipschitzWith C f32private abbrev ModelUnitSphere {n : ℕ} (M : SeminormBall n) := {x : (Fin n → ℝ) // M.p x = 1}3334private def modelOpenBall {n : ℕ} (M : SeminormBall n) : Set ((Fin n → ℝ)) :=35 {x | M.p x < 1}3637private def modelSphereSet {n : ℕ} (M : SeminormBall n) : Set ((Fin n → ℝ)) :=38 {x | M.p x = 1}3940private def segmentPoint {n : ℕ} (x y : (Fin n → ℝ)) (t : ℝ) : (Fin n → ℝ) :=41 (1 - t) • x + t • y4243private theorem exists_segmentPoint_mem_modelSphere {n : ℕ} (M : SeminormBall n)44 {x y : (Fin n → ℝ)} (hx : M.p x < 1) (hy : 1 < M.p y) :45 ∃ t ∈ Set.Icc (0 : ℝ) 1, M.p (segmentPoint x y t) = 1 := by4647 let φ : ℝ → ℝ := fun t => M.p (segmentPoint x y t)48 have hsegment : Continuous (segmentPoint x y) := by49 unfold segmentPoint50 fun_prop51 have hφ : Continuous φ := M.continuous_p.comp hsegment52 have h0 : φ 0 < 1 := by simpa [φ, segmentPoint] using hx53 have h1 : 1 < φ 1 := by simpa [φ, segmentPoint] using hy54 have hone : (1 : ℝ) ∈ Set.Icc (φ 0) (φ 1) := ⟨h0.le, h1.le⟩55 have himage : (1 : ℝ) ∈ φ '' Set.Icc (0 : ℝ) 1 :=56 (intermediate_value_Icc (a := (0 : ℝ)) (b := 1) (f := φ)57 (by norm_num) hφ.continuousOn) hone58 rcases himage with ⟨t, ht, hteq⟩59 exact ⟨t, ht, hteq⟩6061private theorem exists_boundary_point_between {n : ℕ} (M : SeminormBall n)62 {x y : (Fin n → ℝ)} (hx : x ∈ M.unitBall) (hy : y ∉ M.unitBall) :63 ∃ z, M.p z = 1 ∧ ‖x - z‖ ≤ ‖x - y‖ := by6465 by_cases hxs : M.p x = 166 · exact ⟨x, hxs, by simp⟩67 have hxi : M.p x < 1 := lt_of_le_of_ne (M.mem_unitBall.mp hx) hxs68 have hye : 1 < M.p y := lt_of_not_ge (by simpa [SeminormBall.mem_unitBall] using hy)69 rcases exists_segmentPoint_mem_modelSphere M hxi hye with ⟨t, ht, hz⟩70 refine ⟨segmentPoint x y t, hz, ?_⟩71 have ht0 : 0 ≤ t := ht.172 have ht1 : t ≤ 1 := ht.273 rw [segmentPoint]74 have : x - ((1 - t) • x + t • y) = t • (x - y) := by module75 rw [this, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht0]76 exact mul_le_of_le_one_left (norm_nonneg _) ht17778private def zeroExtension {n N : ℕ} (M : SeminormBall n)79 (u : (Fin n → ℝ) → (Fin N → ℝ)) (x : (Fin n → ℝ)) : (Fin N → ℝ) := by80 classical81 exact if x ∈ M.unitBall then u x else 08283@[simp] private theorem zeroExtension_of_mem {n N : ℕ} (M : SeminormBall n)84 (u : (Fin n → ℝ) → (Fin N → ℝ)) {x : (Fin n → ℝ)} (hx : x ∈ M.unitBall) :85 zeroExtension M u x = u x := by86 classical87 simp [zeroExtension, hx]8889@[simp] private theorem zeroExtension_of_not_mem {n N : ℕ} (M : SeminormBall n)90 (u : (Fin n → ℝ) → (Fin N → ℝ)) {x : (Fin n → ℝ)} (hx : x ∉ M.unitBall) :91 zeroExtension M u x = 0 := by92 classical93 simp [zeroExtension, hx]9495private theorem lipschitz_zeroExtension {n N : ℕ} (M : SeminormBall n)96 {u : (Fin n → ℝ) → (Fin N → ℝ)} (hu : Lipschitz u)97 (hbdry : ∀ x, M.p x = 1 → u x = 0) :98 Lipschitz (zeroExtension M u) := by99100 rcases hu with ⟨K, hK⟩101 refine ⟨K, LipschitzWith.of_dist_le_mul ?_⟩102 intro x y103 by_cases hx : x ∈ M.unitBall <;> by_cases hy : y ∈ M.unitBall104 · simpa only [zeroExtension_of_mem M u hx, zeroExtension_of_mem M u hy] using105 hK.dist_le_mul x y106 · rcases exists_boundary_point_between M hx hy with ⟨z, hz, hxz⟩107 have huz : u z = 0 := hbdry z hz108 calc109 dist (zeroExtension M u x) (zeroExtension M u y) = dist (u x) (u z) := by110 rw [zeroExtension_of_mem M u hx, zeroExtension_of_not_mem M u hy, huz]111 _ ≤ (K : ℝ) * dist x z := hK.dist_le_mul x z112 _ ≤ (K : ℝ) * dist x y := by113 apply mul_le_mul_of_nonneg_left ?_ K.2114 simpa only [dist_eq_norm] using hxz115 · rcases exists_boundary_point_between M hy hx with ⟨z, hz, hyz⟩116 have huz : u z = 0 := hbdry z hz117 have hzy : dist z y ≤ dist x y := by118 simpa only [dist_eq_norm, norm_sub_rev] using hyz119 calc120 dist (zeroExtension M u x) (zeroExtension M u y) = dist (u z) (u y) := by121 rw [zeroExtension_of_not_mem M u hx, zeroExtension_of_mem M u hy, huz]122 _ ≤ (K : ℝ) * dist z y := hK.dist_le_mul z y123 _ ≤ (K : ℝ) * dist x y := mul_le_mul_of_nonneg_left hzy K.2124 · rw [zeroExtension_of_not_mem M u hx, zeroExtension_of_not_mem M u hy, dist_self]125 exact mul_nonneg K.2 dist_nonneg126127private theorem support_zeroExtension_subset {n N : ℕ} (M : SeminormBall n)128 (u : (Fin n → ℝ) → (Fin N → ℝ)) :129 Function.support (zeroExtension M u) ⊆ M.unitBall := by130 intro x hx131 by_contra hnot132 exact hx (zeroExtension_of_not_mem M u hnot)133134private theorem hasCompactSupport_zeroExtension {n N : ℕ} (M : SeminormBall n)135 (u : (Fin n → ℝ) → (Fin N → ℝ)) :136 HasCompactSupport (zeroExtension M u) := by137138 exact HasCompactSupport.intro M.isCompact_unitBall fun x hx =>139 zeroExtension_of_not_mem M u hx140141private def boundaryDifference {n N : ℕ}142 (F G : (Fin n → ℝ) → (Fin N → ℝ)) : (Fin n → ℝ) → (Fin N → ℝ) := fun x => F x - G x143144private theorem boundaryDifference_eq_zero {n N : ℕ} (M : SeminormBall n)145 {F G : (Fin n → ℝ) → (Fin N → ℝ)}146 (htrace : ∀ u : ModelUnitSphere M, F u = G u)147 {x : (Fin n → ℝ)} (hx : M.p x = 1) : boundaryDifference F G x = 0 := by148 have h := htrace ⟨x, hx⟩149 simpa [boundaryDifference] using sub_eq_zero.mpr h150151private def patchedMap {n N : ℕ} (M : SeminormBall n)152 (F G : (Fin n → ℝ) → (Fin N → ℝ)) : (Fin n → ℝ) → (Fin N → ℝ) :=153 fun x => G x + zeroExtension M (boundaryDifference F G) x154155@[simp] private theorem patchedMap_eq_of_mem {n N : ℕ} (M : SeminormBall n)156 (F G : (Fin n → ℝ) → (Fin N → ℝ)) {x : (Fin n → ℝ)} (hx : x ∈ M.unitBall) :157 patchedMap M F G x = F x := by158 simp [patchedMap, zeroExtension_of_mem M _ hx, boundaryDifference]159160@[simp] private theorem patchedMap_eq_of_not_mem {n N : ℕ} (M : SeminormBall n)161 (F G : (Fin n → ℝ) → (Fin N → ℝ)) {x : (Fin n → ℝ)} (hx : x ∉ M.unitBall) :162 patchedMap M F G x = G x := by163 simp [patchedMap, zeroExtension_of_not_mem M _ hx]164165private theorem modelSphereSet_null {m : ℕ} (M : SeminormBall (m + 1)) :166 volume (modelSphereSet M) = 0 := by167168 have hsphere :169 modelSphereSet M = frontier (M.p.ball (0 : (Fin (m + 1) → ℝ)) 1) := by170 ext x171 change M.p x = 1 ↔ x ∈ frontier (M.p.ball (0 : (Fin (m + 1) → ℝ)) 1)172 rw [← congrFun M.p.gauge_ball x]173 exact gauge_eq_one_iff_mem_frontier174 (M.p.convex_ball (0 : (Fin (m + 1) → ℝ)) (1 : ℝ))175 (M.p.ball_mem_nhds M.continuous_p zero_lt_one)176 rw [hsphere]177 exact (M.p.convex_ball (0 : (Fin (m + 1) → ℝ)) (1 : ℝ)).addHaar_frontier volume178private theorem integrable_lipschitz_compactPerturb_topMinor_difference_early179 {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))180 {g u : (Fin (m + 1) → ℝ) → (Fin N → ℝ)}181 (hg : Lipschitz g) (hu : Lipschitz u) (huc : HasCompactSupport u) :182 Integrable (fun x =>183 maximalMinorIntegrand s (fun y => g y + u y) x -184 maximalMinorIntegrand s g x) := by185 obtain ⟨Cg, hgW⟩ := hg186 obtain ⟨Cu, huW⟩ := hu187 have hgL : Lipschitz g := ⟨Cg, hgW⟩188 have hplus : Lipschitz (fun x => g x + u x) :=189 ⟨Cg + Cu, hgW.add huW⟩190 let d : (Fin (m + 1) → ℝ) → ℝ := fun x =>191 maximalMinorIntegrand s (fun y => g y + u y) x - maximalMinorIntegrand s g x192 have hdK : IntegrableOn d (tsupport u) := by193 exact (integrableOn_maximalMinor_fderiv_of_lipschitzWith s (hgW.add huW) huc).sub194 (integrableOn_maximalMinor_fderiv_of_lipschitzWith s hgW huc)195 have hdind : Integrable ((tsupport u).indicator d) :=196 hdK.integrable_indicator huc.measurableSet197 have hind : (tsupport u).indicator d = d := by198 funext x199 by_cases hx : x ∈ tsupport u200 · simp [hx]201 · have hz := topMinor_difference_eq_zero_of_not_mem_tsupport202 s (g := g) (u := u) hx203 simpa [hx, d] using hz.symm204 rw [hind] at hdind205 exact hdind206207private theorem topMinor_boundary_trace {m N : ℕ} (M : SeminormBall (m + 1))208 (s : Matrix.MaximalMinorIndex (m + 1) (Fin N)) {F G : (Fin (m + 1) → ℝ) → (Fin N → ℝ)}209 (hF : Lipschitz F) (hG : Lipschitz G)210 (htrace : ∀ u : ModelUnitSphere M, F u = G u) :211 ∫ x in M.unitBall, maximalMinorIntegrand s F x =212 ∫ x in M.unitBall, maximalMinorIntegrand s G x := by213214 let u := boundaryDifference F G215 let u0 := zeroExtension M u216 let H := patchedMap M F G217 let dHG : (Fin (m + 1) → ℝ) → ℝ := fun x =>218 maximalMinorIntegrand s H x - maximalMinorIntegrand s G x219 let dFG : (Fin (m + 1) → ℝ) → ℝ := fun x =>220 maximalMinorIntegrand s F x - maximalMinorIntegrand s G x221 obtain ⟨CF, hFW⟩ := hF222 obtain ⟨CG, hGW⟩ := hG223 have hFL : Lipschitz F := ⟨CF, hFW⟩224 have hGL : Lipschitz G := ⟨CG, hGW⟩225 have hu : Lipschitz u := by226 exact ⟨CF + CG, by227 change LipschitzWith (CF + CG) (fun x => F x - G x)228 exact hFW.sub hGW⟩229 have hub : ∀ x, M.p x = 1 → u x = 0 := by230 intro x hx231 simpa only [u] using boundaryDifference_eq_zero M htrace hx232 have hu0 : Lipschitz u0 := lipschitz_zeroExtension M hu hub233 have huc : HasCompactSupport u0 := hasCompactSupport_zeroExtension M u234 have hglobal : ∫ x, dHG x = 0 := by235 change (∫ x, maximalMinorIntegrand s (fun y => G y + u0 y) x -236 maximalMinorIntegrand s G x) = 0237 rcases hu0 with ⟨C0, h0⟩238 exact integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith s hGW h0 huc239240 have houtside : dHG =ᵐ[volume.restrict (M.unitBall)ᶜ] 0 := by241 filter_upwards [ae_restrict_mem (M.measurableSet_unitBall.compl)] with x hx242 have hlocal : H =ᶠ[𝓝 x] G := by243 have hopen : IsOpen (M.unitBall)ᶜ := M.isClosed_unitBall.isOpen_compl244 filter_upwards [hopen.mem_nhds hx] with y hy245 exact patchedMap_eq_of_not_mem M F G hy246 have hderiv : fderiv ℝ H x = fderiv ℝ G x := hlocal.fderiv_eq247 simp [dHG, maximalMinorIntegrand, hderiv]248249 have hsphere_ae : ∀ᵐ x ∂volume.restrict M.unitBall,250 x ∉ modelSphereSet M := by251 apply ae_restrict_of_ae252 apply ae_iff.mpr253 rw [show {x | ¬ x ∉ modelSphereSet M} = modelSphereSet M by ext z; simp]254 exact modelSphereSet_null M255256 have hinside : dHG =ᵐ[volume.restrict M.unitBall] dFG := by257 filter_upwards [ae_restrict_mem M.measurableSet_unitBall, hsphere_ae]258 with x hx hxsphere259 have hxle : M.p x ≤ 1 := M.mem_unitBall.mp hx260 have hxne : M.p x ≠ 1 := by261 simpa [modelSphereSet] using hxsphere262 have hxi : M.p x < 1 := lt_of_le_of_ne hxle hxne263 have hlocal : H =ᶠ[𝓝 x] F := by264 have hopen : IsOpen (modelOpenBall M) :=265 M.continuous_p.isOpen_preimage _ isOpen_Iio266 have hxopen : x ∈ modelOpenBall M := hxi267 filter_upwards [hopen.mem_nhds hxopen] with y hy268 exact patchedMap_eq_of_mem M F G (M.mem_unitBall.mpr hy.le)269 have hderiv : fderiv ℝ H x = fderiv ℝ F x := hlocal.fderiv_eq270 simp [dHG, dFG, maximalMinorIntegrand, hderiv]271272 have hdiff_integrable : Integrable dHG := by273 change Integrable (fun x =>274 maximalMinorIntegrand s (fun y => G y + u0 y) x -275 maximalMinorIntegrand s G x)276 exact integrable_lipschitz_compactPerturb_topMinor_difference_early s hGL hu0 huc277 have houtside_integral : ∫ x in (M.unitBall)ᶜ, dHG x = 0 := by278 exact MeasureTheory.integral_eq_zero_of_ae houtside279 have hball_integral : ∫ x in M.unitBall, dHG x = 0 := by280 have hsplit :281 (∫ x, dHG x) =282 (∫ x in M.unitBall, dHG x) +283 ∫ x in (M.unitBall)ᶜ, dHG x := by284 exact (integral_add_compl M.measurableSet_unitBall hdiff_integrable).symm285 linarith [hglobal, hsplit, houtside_integral]286 have hFGzero : ∫ x in M.unitBall, dFG x = 0 := by287 rw [← integral_congr_ae hinside]288 exact hball_integral289 have hFi := integrableOn_maximalMinor_fderiv_of_lipschitzWith s hFW M.isCompact_unitBall290 have hGi := integrableOn_maximalMinor_fderiv_of_lipschitzWith s hGW M.isCompact_unitBall291 have hsub :292 (∫ x in M.unitBall, maximalMinorIntegrand s F x) -293 ∫ x in M.unitBall, maximalMinorIntegrand s G x = 0 := by294 simpa [dFG, integral_sub hFi hGi] using hFGzero295 exact sub_eq_zero.mp hsub296297/-- Pointwise equality on a compact seminorm-ball boundary gives equality of maximal-minor integrals. -/298theorem integral_maximalMinor_eq_of_pointwise_boundary_eq299 {m N : ℕ} (p : Seminorm ℝ (Fin (m + 1) → ℝ)) (hp : Continuous p)300 (hK : IsCompact (p.closedBall 0 1))301 (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))302 {F G : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {CF CG : ℝ≥0}303 (hF : LipschitzWith CF F) (hG : LipschitzWith CG G)304 (htrace : ∀ x, p x = 1 → F x = G x) :305 ∫ x in p.closedBall 0 1, maximalMinorIntegrand s F x =306 ∫ x in p.closedBall 0 1, maximalMinorIntegrand s G x := by307 let M : SeminormBall (m + 1) := ⟨p, hp, hK⟩308 exact topMinor_boundary_trace M s ⟨CF, hF⟩ ⟨CG, hG⟩309 (fun x => htrace x x.property)310311end NullLagrangian312end MathlibAnnex