This file introduces the actual L² ambient types used later to package the potential and solenoidal spaces as subspaces of a Hilbert space.

The current Sobolev layer still uses predicate-level MemLp witnesses in many places. This file provides the first typed Lp layer on bounded domains so the closed-subspace and minimization arguments can be formulated cleanly.

@[reducible, inline]

noncomputable abbrev Homogenization.volumeMeasureOn {d : ℕ} (U : Set (Vec d)) : MeasureTheory.Measure (Vec d)

The restricted Lebesgue measure on a domain U ⊆ \R^d.

Equations

• Homogenization.volumeMeasureOn U = MeasureTheory.volume.restrict U

@[reducible, inline]

noncomputable abbrev Homogenization.ScalarL2 {d : ℕ} (U : Set (Vec d)) : AddSubgroup (Vec d →ₘ[volumeMeasureOn U] ℝ)

Scalar-valued L²(U) with respect to restricted Lebesgue measure.

Equations

• Homogenization.ScalarL2 U = MeasureTheory.Lp ℝ 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.VectorL2 {d : ℕ} (U : Set (Vec d)) : AddSubgroup (Vec d →ₘ[volumeMeasureOn U] Vec d)

Vector-valued L²(U; \R^d).

Equations

• Homogenization.VectorL2 U = MeasureTheory.Lp (Homogenization.Vec d) 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.BlockL2 {d : ℕ} (U : Set (Vec d)) : AddSubgroup (Vec d →ₘ[volumeMeasureOn U] BlockVec d)

Block-valued L²(U; \R^{2d}).

Equations

• Homogenization.BlockL2 U = MeasureTheory.Lp (Homogenization.BlockVec d) 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.HilbertVectorL2 {d : ℕ} (U : Set (Vec d)) : AddSubgroup (Vec d →ₘ[volumeMeasureOn U] HilbertVec d)

Hilbert-valued L²(U; \R^d) built from the custom Euclidean carrier HilbertVec d. This is the intended ambient space for Hilbert-space arguments.

Equations

• Homogenization.HilbertVectorL2 U = MeasureTheory.Lp (Homogenization.HilbertVec d) 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.HilbertBlockL2 {d : ℕ} (U : Set (Vec d)) : AddSubgroup (Vec d →ₘ[volumeMeasureOn U] HilbertBlockVec d)

Hilbert-valued L²(U; \R^{2d}) built from the custom Euclidean carrier HilbertBlockVec d. This is the intended ambient space for the doubled \mu-problem.

Equations

• Homogenization.HilbertBlockL2 U = MeasureTheory.Lp (Homogenization.HilbertBlockVec d) 2 (Homogenization.volumeMeasureOn U)

@[instance_reducible]

noncomputable instance Homogenization.instMeasurableSpaceHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} : MeasurableSpace ↥(HilbertVectorL2 U)

Equations

• Homogenization.instMeasurableSpaceHilbertVectorL2 = borel ↥(Homogenization.HilbertVectorL2 U)

instance Homogenization.instBorelSpaceHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} : BorelSpace ↥(HilbertVectorL2 U)

@[reducible, inline]

noncomputable abbrev Homogenization.MemScalarL2 {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) : Prop

Predicate-level scalar L² membership on U.

Equations

• Homogenization.MemScalarL2 U u = MeasureTheory.MemLp u 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.MemVectorL2 {d : ℕ} (U : Set (Vec d)) (f : Vec d → Vec d) : Prop

Predicate-level vector L² membership on U.

Equations

• Homogenization.MemVectorL2 U f = MeasureTheory.MemLp f 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.MemBlockL2 {d : ℕ} (U : Set (Vec d)) (F : Vec d → BlockVec d) : Prop

Predicate-level block L² membership on U.

Equations

• Homogenization.MemBlockL2 U F = MeasureTheory.MemLp F 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.MemHilbertVectorL2 {d : ℕ} (U : Set (Vec d)) (f : Vec d → HilbertVec d) : Prop

Predicate-level Hilbert-vector L² membership on U.

Equations

• Homogenization.MemHilbertVectorL2 U f = MeasureTheory.MemLp f 2 (Homogenization.volumeMeasureOn U)

@[reducible, inline]

noncomputable abbrev Homogenization.MemHilbertBlockL2 {d : ℕ} (U : Set (Vec d)) (F : Vec d → HilbertBlockVec d) : Prop

Predicate-level Hilbert-block L² membership on U.

Equations

• Homogenization.MemHilbertBlockL2 U F = MeasureTheory.MemLp F 2 (Homogenization.volumeMeasureOn U)

def Homogenization.hilbertifyVecField {d : ℕ} (f : Vec d → Vec d) : Vec d → HilbertVec d

Reinterpret a plain vector field as a field valued in the Euclidean Hilbert carrier.

Equations

• Homogenization.hilbertifyVecField f x = Homogenization.HilbertVec.ofVec (f x)

def Homogenization.hilbertifyBlockField {d : ℕ} (F : Vec d → BlockVec d) : Vec d → HilbertBlockVec d

Reinterpret a plain doubled field as a field valued in the Euclidean Hilbert carrier.

Equations

• Homogenization.hilbertifyBlockField F x = Homogenization.HilbertBlockVec.ofBlockVec (F x)

noncomputable def Homogenization.toScalarL2 {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemScalarL2 U u) : ↥(ScalarL2 U)

Promote a scalar MemLp witness to the ambient ScalarL2 type.

Equations

• Homogenization.toScalarL2 hu = MeasureTheory.MemLp.toLp u hu

noncomputable def Homogenization.toVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ↥(VectorL2 U)

Promote a vector MemLp witness to the ambient VectorL2 type.

Equations

• Homogenization.toVectorL2 hf = MeasureTheory.MemLp.toLp f hf

noncomputable def Homogenization.toBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : ↥(BlockL2 U)

Promote a block MemLp witness to the ambient BlockL2 type.

Equations

• Homogenization.toBlockL2 hF = MeasureTheory.MemLp.toLp F hF

theorem Homogenization.memVectorL2_fst_of_memBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : MemVectorL2 U fun (x : Vec d) => (F x).1

Extract L² control of the first block component from block L² control.

theorem Homogenization.memVectorL2_snd_of_memBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : MemVectorL2 U fun (x : Vec d) => (F x).2

Extract L² control of the second block component from block L² control.

theorem Homogenization.memHilbertBlockL2_hilbertifyBlockField {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : MemHilbertBlockL2 U (hilbertifyBlockField F)

Reinterpret a plain block L² witness as a Hilbert-block L² witness.

theorem Homogenization.memHilbertVectorL2_hilbertifyVecField {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemHilbertVectorL2 U (hilbertifyVecField f)

Reinterpret a plain vector L² witness as a Hilbert-vector L² witness.

noncomputable def Homogenization.toHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → HilbertVec d} (hf : MemHilbertVectorL2 U f) : ↥(HilbertVectorL2 U)

Promote a Hilbert-vector MemLp witness to the ambient HilbertVectorL2 type.

Equations

• Homogenization.toHilbertVectorL2 hf = MeasureTheory.MemLp.toLp f hf

noncomputable def Homogenization.toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ↥(HilbertVectorL2 U)

Promote a plain vector MemLp witness directly to the Hilbert-vector ambient type.

Equations

• Homogenization.toHilbertVectorL2OfVecField hf = Homogenization.toHilbertVectorL2 ⋯

noncomputable def Homogenization.toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → HilbertBlockVec d} (hF : MemHilbertBlockL2 U F) : ↥(HilbertBlockL2 U)

Promote a Hilbert-block MemLp witness to the ambient HilbertBlockL2 type.

Equations

• Homogenization.toHilbertBlockL2 hF = MeasureTheory.MemLp.toLp F hF

noncomputable def Homogenization.toHilbertBlockL2OfBlockField {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : ↥(HilbertBlockL2 U)

Promote a plain block MemLp witness directly to the Hilbert-block ambient type.

Equations

• Homogenization.toHilbertBlockL2OfBlockField hF = Homogenization.toHilbertBlockL2 ⋯

theorem Homogenization.coeFn_toScalarL2 {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemScalarL2 U u) : ↑↑(toScalarL2 hu) =ᵐ[volumeMeasureOn U] u

theorem Homogenization.coeFn_toVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ↑↑(toVectorL2 hf) =ᵐ[volumeMeasureOn U] f

theorem Homogenization.coeFn_toBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : ↑↑(toBlockL2 hF) =ᵐ[volumeMeasureOn U] F

theorem Homogenization.coeFn_toHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → HilbertVec d} (hf : MemHilbertVectorL2 U f) : ↑↑(toHilbertVectorL2 hf) =ᵐ[volumeMeasureOn U] f

theorem Homogenization.coeFn_toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ↑↑(toHilbertVectorL2OfVecField hf) =ᵐ[volumeMeasureOn U] hilbertifyVecField f

theorem Homogenization.coeFn_toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → HilbertBlockVec d} (hF : MemHilbertBlockL2 U F) : ↑↑(toHilbertBlockL2 hF) =ᵐ[volumeMeasureOn U] F

theorem Homogenization.coeFn_toHilbertBlockL2OfBlockField {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : ↑↑(toHilbertBlockL2OfBlockField hF) =ᵐ[volumeMeasureOn U] hilbertifyBlockField F

theorem Homogenization.toScalarL2_eq_toScalarL2_iff {d : ℕ} {U : Set (Vec d)} {u v : Vec d → ℝ} (hu : MemScalarL2 U u) (hv : MemScalarL2 U v) : toScalarL2 hu = toScalarL2 hv ↔ u =ᵐ[volumeMeasureOn U] v

theorem Homogenization.toVectorL2_eq_toVectorL2_iff {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : toVectorL2 hf = toVectorL2 hg ↔ f =ᵐ[volumeMeasureOn U] g

theorem Homogenization.toBlockL2_eq_toBlockL2_iff {d : ℕ} {U : Set (Vec d)} {F G : Vec d → BlockVec d} (hF : MemBlockL2 U F) (hG : MemBlockL2 U G) : toBlockL2 hF = toBlockL2 hG ↔ F =ᵐ[volumeMeasureOn U] G

theorem Homogenization.toHilbertVectorL2_eq_toHilbertVectorL2_iff {d : ℕ} {U : Set (Vec d)} {f g : Vec d → HilbertVec d} (hf : MemHilbertVectorL2 U f) (hg : MemHilbertVectorL2 U g) : toHilbertVectorL2 hf = toHilbertVectorL2 hg ↔ f =ᵐ[volumeMeasureOn U] g

theorem Homogenization.toHilbertBlockL2_eq_toHilbertBlockL2_iff {d : ℕ} {U : Set (Vec d)} {F G : Vec d → HilbertBlockVec d} (hF : MemHilbertBlockL2 U F) (hG : MemHilbertBlockL2 U G) : toHilbertBlockL2 hF = toHilbertBlockL2 hG ↔ F =ᵐ[volumeMeasureOn U] G

noncomputable def Homogenization.scalarL2SetIntegralCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (S : Set (Vec d)) (hS : MeasurableSet S) : ↥(ScalarL2 U) →L[ℝ] ℝ

Continuous linear integration over a measurable subset, acting on scalar L²(U) classes.

Equations

• Homogenization.scalarL2SetIntegralCLM S hS = (InnerProductSpace.toDual ℝ ↥(Homogenization.ScalarL2 U)) (MeasureTheory.indicatorConstLp 2 hS ⋯ 1)

noncomputable def Homogenization.hilbertVectorL2CoordSetIntegralCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (S : Set (Vec d)) (hS : MeasurableSet S) (i : Fin d) : ↥(HilbertVectorL2 U) →L[ℝ] ℝ

Continuous linear coordinate integration over a measurable subset, acting on Hilbert-vector L²(U) classes.

Equations

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

@[simp]

theorem Homogenization.scalarL2SetIntegralCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (S : Set (Vec d)) (hS : MeasurableSet S) (f : ↥(ScalarL2 U)) : (scalarL2SetIntegralCLM S hS) f = ∫ (x : Vec d) in S, ↑↑f x ∂volumeMeasureOn U

@[simp]

theorem Homogenization.hilbertVectorL2CoordSetIntegralCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (S : Set (Vec d)) (hS : MeasurableSet S) (i : Fin d) (f : ↥(HilbertVectorL2 U)) : (hilbertVectorL2CoordSetIntegralCLM S hS i) f = ∫ (x : Vec d) in S, (↑↑f x).ofLp i ∂volumeMeasureOn U

noncomputable def Homogenization.vectorL2ToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} : ↥(VectorL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

Transport plain vector L² fields into the Hilbert-vector carrier by applying Vec -> HilbertVec pointwise.

Equations

• Homogenization.vectorL2ToHilbertVectorL2 = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) (Homogenization.HilbertVec.ofVecL d)

noncomputable def Homogenization.hilbertVectorL2ToVectorL2 {d : ℕ} {U : Set (Vec d)} : ↥(HilbertVectorL2 U) →L[ℝ] ↥(VectorL2 U)

Transport Hilbert-vector L² fields back to the plain vector carrier by applying HilbertVec -> Vec pointwise.

Equations

• Homogenization.hilbertVectorL2ToVectorL2 = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) ↑(Homogenization.HilbertVec.continuousLinearEquivVec d)

theorem Homogenization.coeFn_vectorL2ToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (f : ↥(VectorL2 U)) : ↑↑(vectorL2ToHilbertVectorL2 f) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertVec.ofVec (↑↑f x)

theorem Homogenization.coeFn_hilbertVectorL2ToVectorL2 {d : ℕ} {U : Set (Vec d)} (f : ↥(HilbertVectorL2 U)) : ↑↑(hilbertVectorL2ToVectorL2 f) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (↑↑f x).toVec

theorem Homogenization.vectorL2ToHilbertVectorL2_toVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : vectorL2ToHilbertVectorL2 (toVectorL2 hf) = toHilbertVectorL2OfVecField hf

theorem Homogenization.hilbertVectorL2ToVectorL2_toHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : hilbertVectorL2ToVectorL2 (toHilbertVectorL2OfVecField hf) = toVectorL2 hf

theorem Homogenization.toHilbertVectorL2OfVecField_sub {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : toHilbertVectorL2OfVecField ⋯ = toHilbertVectorL2OfVecField hf - toHilbertVectorL2OfVecField hg

theorem Homogenization.toHilbertVectorL2OfVecField_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : toHilbertVectorL2OfVecField ⋯ = toHilbertVectorL2OfVecField hf + toHilbertVectorL2OfVecField hg

theorem Homogenization.hilbertVectorL2ToVectorL2_vectorL2ToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (f : ↥(VectorL2 U)) : hilbertVectorL2ToVectorL2 (vectorL2ToHilbertVectorL2 f) = f

theorem Homogenization.vectorL2ToHilbertVectorL2_hilbertVectorL2ToVectorL2 {d : ℕ} {U : Set (Vec d)} (f : ↥(HilbertVectorL2 U)) : vectorL2ToHilbertVectorL2 (hilbertVectorL2ToVectorL2 f) = f

noncomputable def Homogenization.continuousLinearEquivVectorL2 {d : ℕ} {U : Set (Vec d)} : ↥(VectorL2 U) ≃L[ℝ] ↥(HilbertVectorL2 U)

Continuous linear identification between the plain vector carrier VectorL2 U and the Hilbert-vector carrier HilbertVectorL2 U.

Equations

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

@[simp]

theorem Homogenization.continuousLinearEquivVectorL2_apply {d : ℕ} {U : Set (Vec d)} (f : ↥(VectorL2 U)) : continuousLinearEquivVectorL2 f = vectorL2ToHilbertVectorL2 f

@[simp]

theorem Homogenization.continuousLinearEquivVectorL2_symm_apply {d : ℕ} {U : Set (Vec d)} (f : ↥(HilbertVectorL2 U)) : continuousLinearEquivVectorL2.symm f = hilbertVectorL2ToVectorL2 f

theorem Homogenization.norm_hilbertVectorL2ToVectorL2_le {d : ℕ} {U : Set (Vec d)} : ‖hilbertVectorL2ToVectorL2‖ ≤ 1

theorem Homogenization.norm_toVectorL2_le_toHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → HilbertVec d} (hf : MemHilbertVectorL2 U f) : ‖hilbertVectorL2ToVectorL2 (toHilbertVectorL2 hf)‖ ≤ ‖toHilbertVectorL2 hf‖

theorem Homogenization.norm_toVectorL2_le_toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ‖toVectorL2 hf‖ ≤ ‖toHilbertVectorL2OfVecField hf‖

theorem Homogenization.norm_vectorL2ToHilbertVectorL2_le {d : ℕ} {U : Set (Vec d)} : ‖vectorL2ToHilbertVectorL2‖ ≤ ↑d

theorem Homogenization.norm_toHilbertVectorL2OfVecField_le {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : ‖toHilbertVectorL2OfVecField hf‖ ≤ ↑d * ‖toVectorL2 hf‖

theorem Homogenization.inner_toHilbertVectorL2OfVecField_eq_integral {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : inner ℝ (toHilbertVectorL2OfVecField hf) (toHilbertVectorL2OfVecField hg) = ∫ (x : Vec d) in U, vecDot (f x) (g x)

noncomputable def Homogenization.blockL2ToHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} : ↥(BlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)

Transport plain block L² fields into the Hilbert-block carrier by applying BlockVec -> HilbertBlockVec pointwise.

Equations

• Homogenization.blockL2ToHilbertBlockL2 = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) ↑(Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec d).symm

noncomputable def Homogenization.hilbertBlockL2ToBlockL2 {d : ℕ} {U : Set (Vec d)} : ↥(HilbertBlockL2 U) →L[ℝ] ↥(BlockL2 U)

Transport Hilbert-block L² fields back to the plain block carrier by applying HilbertBlockVec -> BlockVec pointwise.

Equations

• Homogenization.hilbertBlockL2ToBlockL2 = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) ↑(Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec d)

theorem Homogenization.coeFn_blockL2ToHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (F : ↥(BlockL2 U)) : ↑↑(blockL2ToHilbertBlockL2 F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertBlockVec.ofBlockVec (↑↑F x)

theorem Homogenization.coeFn_hilbertBlockL2ToBlockL2 {d : ℕ} {U : Set (Vec d)} (F : ↥(HilbertBlockL2 U)) : ↑↑(hilbertBlockL2ToBlockL2 F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (↑↑F x).toBlockVec

theorem Homogenization.blockL2ToHilbertBlockL2_toBlockL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : blockL2ToHilbertBlockL2 (toBlockL2 hF) = toHilbertBlockL2OfBlockField hF

theorem Homogenization.hilbertBlockL2ToBlockL2_toHilbertBlockL2OfBlockField {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : MemBlockL2 U F) : hilbertBlockL2ToBlockL2 (toHilbertBlockL2OfBlockField hF) = toBlockL2 hF

theorem Homogenization.hilbertBlockL2ToBlockL2_blockL2ToHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (F : ↥(BlockL2 U)) : hilbertBlockL2ToBlockL2 (blockL2ToHilbertBlockL2 F) = F

theorem Homogenization.blockL2ToHilbertBlockL2_hilbertBlockL2ToBlockL2 {d : ℕ} {U : Set (Vec d)} (F : ↥(HilbertBlockL2 U)) : blockL2ToHilbertBlockL2 (hilbertBlockL2ToBlockL2 F) = F

noncomputable def Homogenization.continuousLinearEquivBlockL2 {d : ℕ} {U : Set (Vec d)} : ↥(BlockL2 U) ≃L[ℝ] ↥(HilbertBlockL2 U)

Continuous linear identification between the plain block carrier BlockL2 U and the Hilbert-block carrier HilbertBlockL2 U.

Equations

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

@[simp]

theorem Homogenization.continuousLinearEquivBlockL2_apply {d : ℕ} {U : Set (Vec d)} (F : ↥(BlockL2 U)) : continuousLinearEquivBlockL2 F = blockL2ToHilbertBlockL2 F

@[simp]

theorem Homogenization.continuousLinearEquivBlockL2_symm_apply {d : ℕ} {U : Set (Vec d)} (F : ↥(HilbertBlockL2 U)) : continuousLinearEquivBlockL2.symm F = hilbertBlockL2ToBlockL2 F

noncomputable def Homogenization.hilbertBlockVecPotentialCLM {d : ℕ} : HilbertBlockVec d →L[ℝ] HilbertVec d

Continuous linear projection from a Hilbert block L² field to its potential component.

Equations

• Homogenization.hilbertBlockVecPotentialCLM = { toLinearMap := PiLp.projₗ 2 (fun (x : Fin 2) => Homogenization.HilbertVec d) 0, cont := ⋯ }

noncomputable def Homogenization.hilbertBlockVecFluxCLM {d : ℕ} : HilbertBlockVec d →L[ℝ] HilbertVec d

Continuous linear projection from a Hilbert block vector to its flux component.

Equations

• Homogenization.hilbertBlockVecFluxCLM = { toLinearMap := PiLp.projₗ 2 (fun (x : Fin 2) => Homogenization.HilbertVec d) 1, cont := ⋯ }

@[simp]

theorem Homogenization.hilbertBlockVecPotentialCLM_apply {d : ℕ} (X : HilbertBlockVec d) : hilbertBlockVecPotentialCLM X = X.potential

@[simp]

theorem Homogenization.hilbertBlockVecFluxCLM_apply {d : ℕ} (X : HilbertBlockVec d) : hilbertBlockVecFluxCLM X = X.flux

noncomputable def Homogenization.hilbertBlockL2PotentialCLM {d : ℕ} {U : Set (Vec d)} : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

Continuous linear projection from a Hilbert block L² field to its potential component.

Equations

• Homogenization.hilbertBlockL2PotentialCLM = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) Homogenization.hilbertBlockVecPotentialCLM

noncomputable def Homogenization.hilbertBlockL2FluxCLM {d : ℕ} {U : Set (Vec d)} : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

Continuous linear projection from a Hilbert block L² field to its flux component.

Equations

• Homogenization.hilbertBlockL2FluxCLM = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) Homogenization.hilbertBlockVecFluxCLM

theorem Homogenization.coeFn_hilbertBlockL2PotentialCLM {d : ℕ} {U : Set (Vec d)} (F : ↥(HilbertBlockL2 U)) : ↑↑(hilbertBlockL2PotentialCLM F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (↑↑F x).potential

theorem Homogenization.coeFn_hilbertBlockL2FluxCLM {d : ℕ} {U : Set (Vec d)} (F : ↥(HilbertBlockL2 U)) : ↑↑(hilbertBlockL2FluxCLM F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (↑↑F x).flux

noncomputable def Homogenization.hilbertBlockL2Const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : HilbertBlockVec d →L[ℝ] ↥(HilbertBlockL2 U)

Constant Hilbert block fields as elements of the ambient space L²(U; \R^{2d}).

Equations

• Homogenization.hilbertBlockL2Const = MeasureTheory.Lp.constL 2 (Homogenization.volumeMeasureOn U) ℝ

theorem Homogenization.coeFn_hilbertBlockL2Const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (X : HilbertBlockVec d) : ↑↑(hilbertBlockL2Const X) =ᵐ[volumeMeasureOn U] Function.const (Vec d) X

noncomputable def Homogenization.blockVecToHilbertBlockL2Const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : BlockVec d →L[ℝ] ↥(HilbertBlockL2 U)

Constant algebraic block vectors embedded into the Hilbert-valued ambient space L²(U; \R^{2d}).

Equations

• Homogenization.blockVecToHilbertBlockL2Const = Homogenization.hilbertBlockL2Const ∘SL ↑(Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec d).symm

theorem Homogenization.coeFn_blockVecToHilbertBlockL2Const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (P : BlockVec d) : ↑↑(blockVecToHilbertBlockL2Const P) =ᵐ[volumeMeasureOn U] Function.const (Vec d) (HilbertBlockVec.ofBlockVec P)

noncomputable def Homogenization.hilbertBlockL2OperatorOfBlockMat {d : ℕ} (U : Set (Vec d)) (A : BlockMat d) : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)

A fixed block matrix acts continuously on the ambient Hilbert space L²(U; \R^{2d}) by pointwise application.

Equations

• Homogenization.hilbertBlockL2OperatorOfBlockMat U A = ContinuousLinearMap.compLpL 2 (Homogenization.volumeMeasureOn U) (Homogenization.HilbertBlockVec.applyBlockMat A)

theorem Homogenization.coeFn_hilbertBlockL2OperatorOfBlockMat {d : ℕ} {U : Set (Vec d)} (A : BlockMat d) (F : ↥(HilbertBlockL2 U)) : ↑↑((hilbertBlockL2OperatorOfBlockMat U A) F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (HilbertBlockVec.applyBlockMat A) (↑↑F x)

theorem Homogenization.hilbertBlockL2OperatorOfBlockMat_apply_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (A : BlockMat d) (P : BlockVec d) : (hilbertBlockL2OperatorOfBlockMat U A) (blockVecToHilbertBlockL2Const P) = blockVecToHilbertBlockL2Const (blockMatVecMul A P)