analytic_approximation with the H¹ contraction conjunct

The proof of Section5.analytic_approximation (its helper lemmas are private there and are restated here) with the extra conjunct ‖∇g‖² ≤ ‖∇f‖², from realHeatApprox_gradNormSq_le.

@[instance_reducible]

noncomputable def heatApproxH1MeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• heatApproxH1MeasureSpace1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem heatApproxH1MeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem heatApproxH1IsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.cube_finite : MeasureTheory.volume unitCube < ⊤

theorem AVenhance.Infra.FullTheorem.Uniform.heatApproxH1IsFiniteMeasure4 : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.l2_nonneg (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.transfer_sub {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : Heat.frozenCellToTorusL2 ⋯ = Heat.frozenCellToTorusL2 hf - Heat.frozenCellToTorusL2 hg

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.value_norm {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ‖Heat.frozenCellToTorusL2 hf‖ = √(l2NormSq f)

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.gradient_pos {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (hA : 0 < l2NormSq f) : 0 < gradNormSq Df

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.datumLength_pos {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (hA : 0 < l2NormSq f) : 0 < Section5.datumLength f Df

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.scale_energy {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (hA : 0 < l2NormSq f) : Section5.datumLength f Df ^ 2 * gradNormSq Df = l2NormSq f

theorem AVenhance.Infra.FullTheorem.Uniform.HeatApproxH1.normalization_loss {N M r : ℝ} (hM : 0 ≤ M) (hNM : N ≤ 2 * M) (hr : 0 < r) {n : ℕ} (hn : 1 ≤ n) : ↑n.factorial * (1 / r) ^ n * N ≤ M * (↑n.factorial / (r / 2) ^ n)

theorem AVenhance.Infra.FullTheorem.Uniform.analytic_approximation_gradient {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (hA : 0 < l2NormSq f) {α : ℝ} (hα : 0 < α) (hαsmall : α ≤ 1 / 4) : ∃ (g : Homogenization.Vec 2 → ℝ), Homogenization.MemL2On unitCube g ∧ IsZ2Periodic g ∧ Homogenization.MeanZeroOn unitCube g ∧ ContDiff ℝ (↑⊤) g ∧ IsThetaAnalytic (α * Section5.datumLength f Df / 2) g ∧ l2NormSq (f - g) ≤ α ^ 2 * l2NormSq f ∧ l2NormSq f / 4 ≤ l2NormSq g ∧ gradNormSq (spaceGrad g) ≤ gradNormSq Df

analytic_approximation together with the H¹ contraction ‖∇g‖ ≤ ‖∇f‖.