The proof
Source
Main.lean · 64628 lines · 3.0 MB
Showing the first 500 of 64628 lines. The whole file is 3.0 MB; download it to read the rest.
/- Canonical source assembly. Receipts determine verification status. -/
end Bounty
/- BEGIN M000 -/
section
section
open scoped ENNReal
lemma enorm_sq_eq_ofReal (x : ℝ) : ‖x‖ₑ ^ 2 = ENNReal.ofReal (x ^ 2) := by
rw [← ofReal_norm_eq_enorm, ← ENNReal.ofReal_pow (norm_nonneg _), Real.norm_eq_abs, sq_abs]
lemma enorm_sq_eq_ofReal' {E : Type*} [NormedAddCommGroup E] (x : E) :
‖x‖ₑ ^ 2 = ENNReal.ofReal (‖x‖ ^ 2) := by
rw [← ofReal_norm_eq_enorm, ← ENNReal.ofReal_pow (norm_nonneg _)]
end
end
/- END M000 -/
/- BEGIN M001 -/
section
section
noncomputable section
open scoped ENNReal
namespace PolyaBridge.CoreMinmax
open Set Filter Topology
open scoped InnerProductSpace
variable {V H : Type*}
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [NormedAddCommGroup H] [InnerProductSpace ℝ H]
/-- Density holds simultaneously for every entry of a finite family. -/
theorem dense_core_families (S : Submodule ℝ V) (hS : Dense (S : Set V)) (n : ℕ) :
Dense (Set.pi (Set.univ : Set (Fin n)) (fun _ => (S : Set V))) :=
dense_pi Set.univ (fun _ _ => hS)
/-- Linear synthesis from finite coefficient vectors. -/
def synthesis {n : ℕ} (u : Fin n → V) : (Fin n → ℝ) →ₗ[ℝ] V :=
Fintype.linearCombination ℝ u
theorem synthesis_apply {n : ℕ} (u : Fin n → V) (c : Fin n → ℝ) :
synthesis u c = ∑ i, c i • u i :=
rfl
theorem synthesis_injective {n : ℕ} {u : Fin n → V} (hu : LinearIndependent ℝ u) :
Function.Injective (synthesis u) :=
hu.fintypeLinearCombination_injective
/-! The following interface keeps the energy form separate from the ambient
Hilbert norm. In particular, the `H¹` norm is not substituted for Dirichlet energy. -/
def formRayleigh (B : V →L[ℝ] V →L[ℝ] ℝ) (J : V →L[ℝ] H) (v : V) : ENNReal :=
ENNReal.ofReal (B v v) / ENNReal.ofReal (‖J v‖ ^ 2)
def formMinmaxOn (B : V →L[ℝ] V →L[ℝ] ℝ) (J : V →L[ℝ] H)
(S : Submodule ℝ V) (j : ℕ) : ENNReal :=
⨅ (W : Submodule ℝ V) (_ : W ≤ S) (_ : Module.finrank ℝ W = j),
⨆ (v : V) (_ : v ∈ W) (_ : v ≠ 0), formRayleigh B J v
theorem form_diagonal_smul (B : V →L[ℝ] V →L[ℝ] ℝ) (r : ℝ) (v : V) :
B (r • v) (r • v) = r ^ 2 * B v v := by
simp only [map_smul, ContinuousLinearMap.smul_apply, smul_eq_mul]
ring
/-- Gram approximation for the actual energy form, independently of the norm on `V`. -/
theorem exists_core_form_gram_approx (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (S : Submodule ℝ V) (hS : Dense (S : Set V))
{n : ℕ} (u : Fin n → V) (hu : LinearIndependent ℝ u)
{ε : ℝ} (hε : 0 < ε) :
∃ v : Fin n → V, (∀ i, v i ∈ S) ∧ LinearIndependent ℝ v ∧
(∀ i l, |B (v i) (v l) - B (u i) (u l)| < ε) ∧
(∀ i l, |⟪J (v i), J (v l)⟫_ℝ - ⟪J (u i), J (u l)⟫_ℝ| < ε) := by
classical
have hEnergy : ∀ᶠ v : Fin n → V in 𝓝 u,
∀ i l, |B (v i) (v l) - B (u i) (u l)| < ε := by
apply eventually_all.mpr
intro i
apply eventually_all.mpr
intro l
have hc : Continuous (fun v : Fin n → V =>
|B (v i) (v l) - B (u i) (u l)|) := by fun_prop
exact hc.continuousAt.eventually (gt_mem_nhds (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hε))
have hMass : ∀ᶠ v : Fin n → V in 𝓝 u,
∀ i l, |⟪J (v i), J (v l)⟫_ℝ - ⟪J (u i), J (u l)⟫_ℝ| < ε := by
apply eventually_all.mpr
intro i
apply eventually_all.mpr
intro l
have hc : Continuous (fun v : Fin n → V =>
|⟪J (v i), J (v l)⟫_ℝ - ⟪J (u i), J (u l)⟫_ℝ|) := by fun_prop
exact hc.continuousAt.eventually (gt_mem_nhds (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hε))
obtain ⟨v, hvS, hv⟩ := (dense_core_families S hS n).inter_nhds_nonempty
(hu.eventually.and (hEnergy.and hMass))
exact ⟨v, (fun i => hvS i (Set.mem_univ i)), hv.1, hv.2.1, hv.2.2⟩
theorem eventually_trial_form_bound (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J) {n : ℕ}
(u : Fin n → V) (hu : LinearIndependent ℝ u) {A C : ℝ} (hAC : A < C)
(hA : ∀ c : Fin n → ℝ,
B (synthesis u c) (synthesis u c) ≤ A * ‖J (synthesis u c)‖ ^ 2) :
∀ᶠ v : Fin n → V in 𝓝 u, ∀ c : Fin n → ℝ,
B (synthesis v c) (synthesis v c) ≤ C * ‖J (synthesis v c)‖ ^ 2 := by
classical
have hSphere : ∀ᶠ v : Fin n → V in 𝓝 u,
∀ c ∈ Metric.sphere (0 : Fin n → ℝ) 1,
B (synthesis v c) (synthesis v c) < C * ‖J (synthesis v c)‖ ^ 2 := by
apply (isCompact_sphere (0 : Fin n → ℝ) 1).eventually_forall_of_forall_eventually
intro c hc
have hcNorm : ‖c‖ = 1 := by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hc
have hc0 : c ≠ 0 := by
intro hc0
simp [_root_.PolyaBridge.CoreMinmax.synthesis_apply, hc0] at hcNorm
have huc0 : synthesis u c ≠ 0 := by
intro hz
exact hc0 ((synthesis_injective hu) (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hz))
have hJuc0 : J (synthesis u c) ≠ 0 := by
intro hz
exact huc0 (hJ (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hz))
have hMassPos : 0 < ‖J (synthesis u c)‖ ^ 2 := by positivity
have hStrict : B (synthesis u c) (synthesis u c) <
C * ‖J (synthesis u c)‖ ^ 2 :=
(hA c).trans_lt (mul_lt_mul_of_pos_right hAC hMassPos)
have hEnergyCont : Continuous (fun p : (Fin n → V) × (Fin n → ℝ) =>
B (synthesis p.1 p.2) (synthesis p.1 p.2)) := by
simp only [synthesis_apply]
fun_prop
have hMassCont : Continuous (fun p : (Fin n → V) × (Fin n → ℝ) =>
C * ‖J (synthesis p.1 p.2)‖ ^ 2) := by
simp only [synthesis_apply]
fun_prop
exact (isOpen_lt hEnergyCont hMassCont).mem_nhds hStrict
filter_upwards [hSphere] with v hv c
by_cases hc0 : c = 0
· simp [_root_.PolyaBridge.CoreMinmax.synthesis_apply, hc0]
have hcPos : 0 < ‖c‖ := norm_pos_iff.mpr hc0
let d : Fin n → ℝ := ‖c‖⁻¹ • c
have hdSphere : d ∈ Metric.sphere (0 : Fin n → ℝ) 1 := by
rw [Metric.mem_sphere, dist_zero_right]
simp only [d, norm_smul, Real.norm_eq_abs, abs_inv, abs_norm,
inv_mul_cancel₀ hcPos.ne']
have hd := hv d hdSphere
have hSynth : synthesis v d = ‖c‖⁻¹ • synthesis v c := by
exact (synthesis v).map_smul ‖c‖⁻¹ c
rw [hSynth, form_diagonal_smul, J.map_smul] at hd
simp only [norm_smul, Real.norm_eq_abs, abs_inv, abs_norm, mul_pow] at hd
have hd' : (‖c‖⁻¹) ^ 2 * B (synthesis v c) (synthesis v c) <
(‖c‖⁻¹) ^ 2 * (C * ‖J (synthesis v c)‖ ^ 2) := by
simpa only [mul_assoc, mul_left_comm] using hd
exact ((mul_lt_mul_iff_right₀ (by positivity : 0 < (‖c‖⁻¹) ^ 2)).mp hd').le
theorem formRayleigh_le_of_energy_bound (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) {v : V} {C : ℝ} (hC : 0 ≤ C)
(hBound : B v v ≤ C * ‖J v‖ ^ 2) :
formRayleigh B J v ≤ ENNReal.ofReal C := by
apply ENNReal.div_le_of_le_mul
rw [← ENNReal.ofReal_mul hC]
exact ENNReal.ofReal_le_ofReal hBound
theorem exists_core_trial_form_rayleigh_bound (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J)
(S : Submodule ℝ V) (hS : Dense (S : Set V))
{n : ℕ} (u : Fin n → V) (hu : LinearIndependent ℝ u)
{A C : ℝ} (hAC : A < C) (hC : 0 ≤ C)
(hA : ∀ c : Fin n → ℝ,
B (synthesis u c) (synthesis u c) ≤ A * ‖J (synthesis u c)‖ ^ 2) :
∃ W : Submodule ℝ V, W ≤ S ∧ Module.finrank ℝ W = n ∧
∀ x ∈ W, formRayleigh B J x ≤ ENNReal.ofReal C := by
have hBound := eventually_trial_form_bound B J hJ u hu hAC hA
obtain ⟨v, hvS, hv⟩ := (dense_core_families S hS n).inter_nhds_nonempty
(hu.eventually.and hBound)
refine ⟨Submodule.span ℝ (Set.range v), ?_, ?_, ?_⟩
· apply Submodule.span_le.mpr
rintro _ ⟨i, rfl⟩
exact hvS i (Set.mem_univ i)
· rw [finrank_span_eq_card hv.1, Fintype.card_fin]
· intro x hx
obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℝ).mp hx
apply formRayleigh_le_of_energy_bound B J hC
have hxc : synthesis v c = x := by simpa only [synthesis_apply] using hc
simpa only [hxc] using hv.2 c
theorem core_formMinmax_le_of_trial_energy_bound (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J)
(S : Submodule ℝ V) (hS : Dense (S : Set V))
{n : ℕ} (u : Fin n → V) (hu : LinearIndependent ℝ u)
{A C : ℝ} (hAC : A < C) (hC : 0 ≤ C)
(hA : ∀ c : Fin n → ℝ,
B (synthesis u c) (synthesis u c) ≤ A * ‖J (synthesis u c)‖ ^ 2) :
formMinmaxOn B J S n ≤ ENNReal.ofReal C := by
obtain ⟨W, hWS, hWdim, hWBound⟩ :=
exists_core_trial_form_rayleigh_bound B J hJ S hS u hu hAC hC hA
calc
formMinmaxOn B J S n ≤
⨆ (x : V) (_ : x ∈ W) (_ : x ≠ 0), formRayleigh B J x :=
iInf_le_of_le W (iInf_le_of_le hWS (iInf_le_of_le hWdim le_rfl))
_ ≤ ENNReal.ofReal C :=
iSup_le fun x => iSup_le fun hx => iSup_le fun _ => hWBound x hx
/-- Supremum of the Rayleigh quotient on a fixed trial space. -/
def formTrialSup (B : V →L[ℝ] V →L[ℝ] ℝ) (J : V →L[ℝ] H)
(W : Submodule ℝ V) : ENNReal :=
⨆ (v : V) (_ : v ∈ W) (_ : v ≠ 0), formRayleigh B J v
theorem form_energy_bound_of_rayleigh_le (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J) {v : V} {A : ℝ}
(hA : 0 ≤ A) (hRayleigh : formRayleigh B J v ≤ ENNReal.ofReal A) :
B v v ≤ A * ‖J v‖ ^ 2 := by
by_cases hv0 : v = 0
· simp [_root_.PolyaBridge.CoreMinmax.synthesis_apply, hv0]
have hJv0 : J v ≠ 0 := by
intro hz
exact hv0 (hJ (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hz))
have hMassPos : 0 < ‖J v‖ ^ 2 := by positivity
have hMass0 : ENNReal.ofReal (‖J v‖ ^ 2) ≠ 0 :=
ne_of_gt (ENNReal.ofReal_pos.mpr hMassPos)
have hMassTop : ENNReal.ofReal (‖J v‖ ^ 2) ≠ ⊤ := ENNReal.ofReal_ne_top
have hEnergy : ENNReal.ofReal (B v v) ≤
ENNReal.ofReal A * ENNReal.ofReal (‖J v‖ ^ 2) :=
(ENNReal.div_le_iff hMass0 hMassTop).mp hRayleigh
rw [← ENNReal.ofReal_mul hA] at hEnergy
exact (ENNReal.ofReal_le_ofReal_iff (mul_nonneg hA (sq_nonneg _))).mp hEnergy
/-- The core min-max is bounded by the Rayleigh supremum of any finite-dimensional
trial space. The finite bound case is obtained by approximation and order density;
an infinite trial supremum needs no approximation. -/
theorem core_formMinmax_le_trialSup (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J)
(S : Submodule ℝ V) (hS : Dense (S : Set V))
{j : ℕ} (hj : 0 < j) (W : Submodule ℝ V) (hWdim : Module.finrank ℝ W = j) :
formMinmaxOn B J S j ≤ formTrialSup B J W := by
classical
by_cases hTop : formTrialSup B J W = ⊤
· rw [hTop]
exact le_top
letI : Module.IsTorsionFree ℝ W := DivisionSemiring.to_moduleIsTorsionFree
letI : Module.Finite ℝ W := Module.finite_of_finrank_pos (by
rw [hWdim]
exact hj)
let b := Module.finBasisOfFinrankEq ℝ W hWdim
let u : Fin j → V := fun i => (b i : V)
have hu : LinearIndependent ℝ u := by
exact b.linearIndependent.map' W.subtype (Submodule.ker_subtype W)
have hMem : ∀ c : Fin j → ℝ, synthesis u c ∈ W := by
intro c
rw [synthesis_apply]
exact W.sum_mem fun i _ => W.smul_mem (c i) (b i).property
have hRayleigh : ∀ c : Fin j → ℝ,
formRayleigh B J (synthesis u c) ≤ formTrialSup B J W := by
intro c
by_cases hc0 : synthesis u c = 0
· simp [_root_.PolyaBridge.CoreMinmax.synthesis_apply, hc0, formRayleigh]
· exact le_iSup_of_le (synthesis u c)
(le_iSup_of_le (hMem c) (le_iSup_of_le hc0 le_rfl))
have hA : ∀ c : Fin j → ℝ,
B (synthesis u c) (synthesis u c) ≤
(formTrialSup B J W).toReal * ‖J (synthesis u c)‖ ^ 2 := by
intro c
apply form_energy_bound_of_rayleigh_le B J hJ ENNReal.toReal_nonneg
simpa only [ENNReal.ofReal_toReal hTop] using hRayleigh c
apply le_of_forall_gt_imp_ge_of_dense
intro C hC
by_cases hCTop : C = ⊤
· rw [hCTop]
exact le_top
have hAC : (formTrialSup B J W).toReal < C.toReal :=
(ENNReal.toReal_lt_toReal hTop hCTop).mpr hC
have hBound := core_formMinmax_le_of_trial_energy_bound B J hJ S hS u hu
hAC ENNReal.toReal_nonneg hA
simpa only [ENNReal.ofReal_toReal hCTop] using hBound
/-- A dense form core has exactly the same positive-index min-max values as the
whole form domain. The energy remains the supplied continuous bilinear form. -/
theorem formMinmaxOn_eq_top_of_dense (B : V →L[ℝ] V →L[ℝ] ℝ)
(J : V →L[ℝ] H) (hJ : Function.Injective J)
(S : Submodule ℝ V) (hS : Dense (S : Set V)) {j : ℕ} (hj : 0 < j) :
formMinmaxOn B J S j = formMinmaxOn B J ⊤ j := by
apply le_antisymm
· unfold formMinmaxOn
refine le_iInf fun W => le_iInf fun _ => le_iInf fun hWdim => ?_
exact core_formMinmax_le_trialSup B J hJ S hS hj W hWdim
· unfold formMinmaxOn
refine le_iInf fun W => le_iInf fun _ => le_iInf fun hWdim => ?_
exact iInf_le_of_le W
(iInf_le_of_le (le_top : W ≤ ⊤) (iInf_le_of_le hWdim le_rfl))
end PolyaBridge.CoreMinmax
namespace DirichletBridge.MinmaxTransport
variable {U W : Type*} [AddCommGroup U] [Module ℝ U] [AddCommGroup W] [Module ℝ W]
def minmax (S : Submodule ℝ U) (R : U → ENNReal) (j : ℕ) : ENNReal :=
⨅ (V : Submodule ℝ U) (_ : V ≤ S) (_ : Module.finrank ℝ V = j),
⨆ (u : U) (_ : u ∈ V) (_ : u ≠ 0), R u
theorem le_of_map {S : Submodule ℝ U} {T : Submodule ℝ W}
{R : U → ENNReal} {Q : W → ENNReal} (P : U →ₗ[ℝ] W)
(hPT : ∀ u ∈ S, P u ∈ T)
(hinj : ∀ u ∈ S, P u = 0 → u = 0)
(hR : ∀ u ∈ S, u ≠ 0 → Q (P u) ≤ R u) (j : ℕ) :
minmax T Q j ≤ minmax S R j := by
classical
unfold minmax
refine le_iInf fun V => le_iInf fun hV => le_iInf fun hj => ?_
have hinjV : Function.Injective (P.domRestrict V) := by
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
intro x hx
exact Subtype.ext (hinj x (hV x.property) (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hx))
let Z := LinearMap.range (P.domRestrict V)
have hZdim : Module.finrank ℝ Z = j := by
rw [LinearMap.finrank_range_of_inj hinjV, hj]
have hZT : Z ≤ T := by
rintro _ ⟨x, rfl⟩
exact hPT x (hV x.property)
apply (iInf_le_of_le Z (iInf_le_of_le hZT (iInf_le_of_le hZdim le_rfl))).trans
refine iSup_le fun v => iSup_le fun hv => iSup_le fun hv0 => ?_
obtain ⟨x, rfl⟩ := hv
have hx0 : (x : U) ≠ 0 := by
rintro h
apply hv0
simp [_root_.PolyaBridge.CoreMinmax.synthesis_apply, h]
exact (hR x (hV x.property) hx0).trans
(le_iSup_of_le (x : U) (le_iSup_of_le x.property (le_iSup_of_le hx0 le_rfl)))
theorem eq_range_of_injective (P : U →ₗ[ℝ] W) (hP : Function.Injective P)
(R : U → ENNReal) (Q : W → ENNReal) (hR : ∀ u, Q (P u) = R u) (j : ℕ) :
minmax P.range Q j = minmax ⊤ R j := by
obtain ⟨L, hL⟩ := P.exists_leftInverse_of_injective (LinearMap.ker_eq_bot.mpr hP)
have hLP : ∀ u, L (P u) = u := by
intro u
exact congrArg (fun f : U →ₗ[ℝ] U => f u) hL
apply le_antisymm
· exact le_of_map (S := ⊤) (T := P.range) P (fun u _ => ⟨u, rfl⟩)
(fun u _ hu => hP (by simpa [_root_.PolyaBridge.CoreMinmax.synthesis_apply] using hu)) (fun u _ _ => (hR u).le) j
· apply le_of_map (S := P.range) (T := ⊤) L (fun _ _ => Submodule.mem_top)
· rintro v ⟨u, rfl⟩ hu
rw [hLP] at hu
rw [hu, map_zero]
· rintro v ⟨u, rfl⟩ _
rw [hLP, hR]
end DirichletBridge.MinmaxTransport
end
end
end
/- END M001 -/
/- BEGIN M002 -/
section
section
noncomputable section
open Set MeasureTheory
open scoped ENNReal NNReal Topology ContDiff
namespace Math30.Polya.TangWangBridge
def planeTestFunctions (Ω : Set Plane) : Submodule ℝ (Plane → ℝ) where
carrier := {u | IsTestFunction Ω u}
zero_mem' := ⟨contDiff_const, HasCompactSupport.zero, by simp⟩
add_mem' := by
rintro u v ⟨hu, hu', hu''⟩ ⟨hv, hv', hv''⟩
exact ⟨hu.add hv, hu'.add hv', (tsupport_add u v).trans (Set.union_subset hu'' hv'')⟩
smul_mem' := by
rintro c u ⟨hu, hu', hu''⟩
exact ⟨hu.const_smul c, HasCompactSupport.smul_left (f := fun _ => c) hu',
(tsupport_smul_subset_right (fun _ => c) u).trans hu''⟩
def planeRayleigh (u : Plane → ℝ) : ℝ≥0∞ :=
(∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ 2) / (∫⁻ x, ‖u x‖ₑ ^ 2)
def planeSmoothEigenvalue (Ω : Set Plane) (k : ℕ) : ℝ≥0∞ :=
DirichletBridge.MinmaxTransport.minmax (planeTestFunctions Ω) planeRayleigh k
theorem norm_gradient_eq_fderiv (u : Plane → ℝ) (x : Plane) :
‖gradient u x‖ = ‖fderiv ℝ u x‖ :=
(InnerProductSpace.toDual ℝ Plane).symm.norm_map _
theorem enorm_gradient_eq_fderiv (u : Plane → ℝ) (x : Plane) :
‖gradient u x‖ₑ = ‖fderiv ℝ u x‖ₑ := by
apply ENNReal.coe_inj.mpr
exact NNReal.eq (norm_gradient_eq_fderiv u x)
end Math30.Polya.TangWangBridge
end
end
end
/- END M002 -/
/- BEGIN M003 -/
section
section
noncomputable section
open Set MeasureTheory Topology
open scoped ENNReal InnerProductSpace
namespace Math30.Polya.GraphMinmaxBridge
open DirichletBridge.MinmaxTransport
theorem trialSup_eq_flat {Ω : Set Plane} {k : ℕ} (V : TrialSpace Ω k) :
trialSup V = ⨆ (w : SobolevAmbient) (_ : w ∈ V.space) (_ : w ≠ 0), rayleigh w := by
apply le_antisymm
· refine iSup_le fun w => ?_
exact le_iSup_of_le w.val (le_iSup_of_le w.property.1
(le_iSup_of_le w.property.2 le_rfl))
· refine iSup_le fun w => iSup_le fun hw => iSup_le fun hw0 => ?_
exact le_iSup (fun w : {w : SobolevAmbient // w ∈ V.space ∧ w ≠ 0} => rayleigh w.val)
⟨w, hw, hw0⟩
theorem dirichletMinmax_eq_submoduleMinmax (Ω : Set Plane) {k : ℕ} (hk : 0 < k) :
dirichletMinmax Ω k = minmax (h01Submodule Ω) rayleigh k := by
apply le_antisymm
· unfold DirichletBridge.MinmaxTransport.minmax
refine le_iInf fun W => le_iInf fun hW => le_iInf fun hdim => ?_
letI : FiniteDimensional ℝ W := Module.finite_of_finrank_pos (hdim.symm ▸ hk)
let V : TrialSpace Ω k := ⟨W, inferInstance, hdim, hW⟩
exact (dirichletMinmax_le_trialSup V).trans_eq (trialSup_eq_flat V)
· unfold dirichletMinmax
refine le_iInf fun V => ?_
unfold DirichletBridge.MinmaxTransport.minmax
exact (iInf_le_of_le V.space (iInf_le_of_le V.contained
(iInf_le_of_le V.dimension le_rfl))).trans_eq (trialSup_eq_flat V).symm
theorem minmax_map_of_injective {U W : Type*} [AddCommGroup U] [Module ℝ U]
[AddCommGroup W] [Module ℝ W] (P : U →ₗ[ℝ] W) (hP : Function.Injective P)
(S : Submodule ℝ U) (R : U → ENNReal) (Q : W → ENNReal)
(hR : ∀ u, Q (P u) = R u) (k : ℕ) :
minmax (S.map P) Q k = minmax S R k := by
have hSubtype := eq_range_of_injective S.subtype Subtype.val_injective
(fun u : S => R u) R (fun _ => rfl) k
have hMap := eq_range_of_injective (P.comp S.subtype)
(hP.comp Subtype.val_injective) (fun u : S => R u) Q (fun u => hR u) k
rw [Submodule.range_subtype] at hSubtype
rw [LinearMap.range_comp, Submodule.range_subtype] at hMap
exact hMap.trans hSubtype.symm
abbrev HilbertAmbient := WithLp 2 SobolevAmbient
def ambientEquiv : HilbertAmbient ≃L[ℝ] SobolevAmbient :=
WithLp.prodContinuousLinearEquiv 2 ℝ
(Lp ℝ 2 (volume : Measure Plane)) (Lp Plane 2 (volume : Measure Plane))
def hilbertGraph (Ω : Set Plane) : Submodule ℝ HilbertAmbient :=
(h01Submodule Ω).comap ambientEquiv.toLinearMap
abbrev HilbertGraph (Ω : Set Plane) := hilbertGraph Ω
def graphProjection (Ω : Set Plane) : HilbertGraph Ω →L[ℝ] SobolevAmbient :=
ambientEquiv.toContinuousLinearMap.comp (hilbertGraph Ω).subtypeL
def graphValue (Ω : Set Plane) : HilbertGraph Ω →L[ℝ] Lp ℝ 2 (volume : Measure Plane) :=
(ContinuousLinearMap.fst ℝ _ _).comp (graphProjection Ω)
def graphGradient (Ω : Set Plane) :
HilbertGraph Ω →L[ℝ] Lp Plane 2 (volume : Measure Plane) :=
(ContinuousLinearMap.snd ℝ _ _).comp (graphProjection Ω)
def graphEnergyForm (Ω : Set Plane) : HilbertGraph Ω →L[ℝ] HilbertGraph Ω →L[ℝ] ℝ :=
(innerSL ℝ).bilinearComp (graphGradient Ω) (graphGradient Ω)
theorem graphProjection_injective (Ω : Set Plane) :
Function.Injective (graphProjection Ω) := by
intro u v h
apply Subtype.ext
exact ambientEquiv.injective h
theorem graphValue_injective (Ω : Set Plane) : Function.Injective (graphValue Ω) := by
intro u v h
apply graphProjection_injective Ω
exact h01Graph_fst_injective Ω u.property v.property h
theorem formRayleigh_eq (Ω : Set Plane) (u : HilbertGraph Ω) :
PolyaBridge.CoreMinmax.formRayleigh (graphEnergyForm Ω) (graphValue Ω) u =
rayleigh (graphProjection Ω u) := by
simp only [PolyaBridge.CoreMinmax.formRayleigh, graphEnergyForm,
ContinuousLinearMap.bilinearComp_apply, innerSL_apply_apply,
real_inner_self_eq_norm_sq]Provenance