Coarse-graining support: Support.Sobolev.Foundations.CoerciveH1Dilation

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.map_smul_volume_restrict {d : ℕ} {a : ℝ} (ha : 0 < a) (U : Set (Vec d)) : MeasureTheory.Measure.map (fun (x : Vec d) => a • x) (MeasureTheory.volume.restrict U) = ENNReal.ofReal (a ^ d)⁻¹ • MeasureTheory.volume.restrict (a • U)

Scaling by a positive scalar maps restricted Lebesgue measure on U to the corresponding scalar multiple of restricted Lebesgue measure on a • U.

noncomputable def HCPolySupport.H1Function.dilate {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function U) : H1Function (a • U)

Push an H¹(U) witness forward to H¹(a • U) by the dilation x ↦ a⁻¹ x, with the value normalized by the factor a. With this normalization the gradient is the plain pullback of the original gradient.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.dilate_toFun {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function U) (x : Vec d) : (dilate ha u).toFun x = a * u.toFun (a⁻¹ • x)

@[simp]

theorem HCPolySupport.H1Function.dilate_grad {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function U) (x : Vec d) : (dilate ha u).grad x = u.grad (a⁻¹ • x)

noncomputable def HCPolySupport.H1Function.dilateSet {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function U) : H1Function V

Push an H¹(U) witness forward to any domain V that is propositionally equal to a • U. This avoids casts when geometric APIs identify the dilated set by an extensional equality.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.dilateSet_toFun {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function U) (x : Vec d) : (dilateSet ha hV u).toFun x = a * u.toFun (a⁻¹ • x)

@[simp]

theorem HCPolySupport.H1Function.dilateSet_grad {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function U) (x : Vec d) : (dilateSet ha hV u).grad x = u.grad (a⁻¹ • x)

noncomputable def HCPolySupport.H1Function.unscale {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) : H1Function U

Pull an H¹(a • U) witness back to H¹(U) by precomposition with x ↦ a • x. The weak gradient is a • ∇u(a x).

Equations

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

@[simp]

theorem HCPolySupport.H1Function.unscale_toFun {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) (x : Vec d) : (unscale ha u).toFun x = u.toFun (a • x)

@[simp]

theorem HCPolySupport.H1Function.unscale_grad {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) (x : Vec d) : (unscale ha u).grad x = a • u.grad (a • x)

noncomputable def HCPolySupport.H1Function.undilateSet {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function V) : H1Function U

Pull an H¹(V) witness back to H¹(U) when V = a • U, with the normalization inverse to H1Function.dilateSet: u(a x) / a.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.undilateSet_toFun {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function V) (x : Vec d) : (undilateSet ha hV u).toFun x = a⁻¹ * u.toFun (a • x)

@[simp]

theorem HCPolySupport.H1Function.undilateSet_grad {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) (u : H1Function V) (x : Vec d) : (undilateSet ha hV u).grad x = u.grad (a • x)

noncomputable def HCPolySupport.H10Function.unscale {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H10Function (a • U)) : H10Function U

Pull an H¹₀(a • U) witness back to H¹₀(U) by precomposition with x ↦ a x.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.unscale_toH1Function {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H10Function (a • U)) : (unscale ha u).toH1Function = H1Function.unscale ha u.toH1Function

noncomputable def HCPolySupport.dilationL2Factor (d : ℕ) (a : ℝ) : ℝ

The common L² measure factor produced by pulling back along x ↦ a • x.

Equations

• HCPolySupport.dilationL2Factor d a = (ENNReal.ofReal (a ^ d)⁻¹ ^ (1 / 2).toReal).toReal

theorem HCPolySupport.dilationL2Factor_eq {d : ℕ} {a : ℝ} (ha : 0 < a) : dilationL2Factor d a = (a ^ d)⁻¹ ^ (1 / 2)

theorem HCPolySupport.dilationL2Factor_pos {d : ℕ} {a : ℝ} (ha : 0 < a) : 0 < dilationL2Factor d a

theorem HCPolySupport.H1Function.norm_toScalarL2_unscale_eq {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) : ‖(unscale ha u).toScalarL2‖ = dilationL2Factor d a * ‖u.toScalarL2‖

The scalar L² norm of an H¹ function after dilation pullback.

theorem HCPolySupport.H1Function.norm_gradCoordToScalarL2_unscale_eq {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) (i : Fin d) : ‖(unscale ha u).gradCoordToScalarL2 i‖ = a * dilationL2Factor d a * ‖u.gradCoordToScalarL2 i‖

The coordinate-gradient L² norm of an H¹ function after dilation pullback.

theorem HCPolySupport.H1Function.gradientCoordL2NormSum_unscale_eq {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1Function (a • U)) : (unscale ha u).gradientCoordL2NormSum = a * dilationL2Factor d a * u.gradientCoordL2NormSum

The coordinate-gradient norm sum after dilation pullback.

noncomputable def HCPolySupport.H1MeanZeroFunction.unscale {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) : H1MeanZeroFunction U

Pull a mean-zero H¹(a • U) witness back to H¹(U).

Equations

• HCPolySupport.H1MeanZeroFunction.unscale ha u = { toH1Function := HCPolySupport.H1Function.unscale ha u.toH1Function, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.unscale_toH1Function {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) : (unscale ha u).toH1Function = H1Function.unscale ha u.toH1Function

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.unscale_apply {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) (x : Vec d) : (unscale ha u).toH1Function.toFun x = u.toH1Function.toFun (a • x)

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.unscale_grad {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) (x : Vec d) : (unscale ha u).toH1Function.grad x = a • u.toH1Function.grad (a • x)

theorem HCPolySupport.H1MeanZeroFunction.valueL2Norm_unscale_eq {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) : (unscale ha u).valueL2Norm = dilationL2Factor d a * u.valueL2Norm

The scalar L² norm after dilation pullback.

theorem HCPolySupport.H1MeanZeroFunction.gradientL2Norm_unscale_eq {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (u : H1MeanZeroFunction (a • U)) : (unscale ha u).gradientL2Norm = a * dilationL2Factor d a * u.gradientL2Norm

The gradient L² norm after dilation pullback.

noncomputable def HCPolySupport.H1CoerciveEstimate.dilate {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hC : H1CoerciveEstimate U) : H1CoerciveEstimate (a • U)

Dilation transports a mean-zero coercive H¹ estimate from U to a • U, multiplying the constant by the dilation factor a.

Equations

• HCPolySupport.H1CoerciveEstimate.dilate ha hC = { constantValue := a * hC.constantValue, constant_nonneg := ⋯, bound := ⋯ }

@[simp]

theorem HCPolySupport.H1CoerciveEstimate.dilate_constant {d : ℕ} {U : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hC : H1CoerciveEstimate U) : (dilate ha hC).constantValue = a * hC.constantValue