Conditional H1-to-analytic reduction. Analytic dissipation and weak-solution energy are inputs, not assertions that the corresponding PDE gates are proved.

@[instance_reducible]

noncomputable def avInfraSection5H1ReductionMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraSection5H1ReductionMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraSection5H1ReductionIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Section5.H1Reduction.cube_finite : MeasureTheory.volume unitCube < ⊤

theorem AVenhance.Infra.Section5.avInfraSection5H1ReductionIsFiniteMeasure4 : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.H1Reduction.l2_nonneg (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.Section5.H1Reduction.grad_nonneg (Df : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq Df

theorem AVenhance.Infra.Section5.H1Reduction.st_nonneg (Df : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ spaceTimeGradNormSq Df

theorem AVenhance.Infra.Section5.H1Reduction.memL2_real_pullback (G : C(UnitAddTorus (Fin 2), ℂ)) : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => (G (Torus.toUnitTorus 2 x)).re

noncomputable def AVenhance.Infra.Section5.realHeatApprox {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : Homogenization.Vec 2 → ℝ

A real smooth representative of the datum's heat evolution.

Equations

• AVenhance.Infra.Section5.realHeatApprox hf hs x = (AVenhance.Infra.Heat.heatTorusSmoothLift hs (AVenhance.Infra.Heat.frozenPeriodicH1ValueL2 hf) x).re

theorem AVenhance.Infra.Section5.H1Reduction.realHeatApprox_eq {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : realHeatApprox hf hs = fun (x : Homogenization.Vec 2) => ((Heat.heatTorusContinuous hs (Heat.frozenPeriodicH1ValueL2 hf)) (Torus.toUnitTorus 2 x)).re

theorem AVenhance.Infra.Section5.realHeatApprox_memL2 {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : Homogenization.MemL2On unitCube (realHeatApprox hf hs)

theorem AVenhance.Infra.Section5.realHeatApprox_periodic {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : IsZ2Periodic (realHeatApprox hf hs)

theorem AVenhance.Infra.Section5.H1Reduction.transfer_sub_realHeat_norm_le {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : ‖Heat.frozenCellToTorusL2 ⋯‖ ≤ ‖Heat.frozenPeriodicH1ValueL2 hf - Heat.heatTorusL2 s ⋯ (Heat.frozenPeriodicH1ValueL2 hf)‖

theorem AVenhance.Infra.Section5.realHeatApprox_error_sq {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : (l2NormSq fun (x : Homogenization.Vec 2) => f x - realHeatApprox hf hs x) ≤ s * gradNormSq Df

the distance estimate: the missing distance estimate, in the actual real carriers.

theorem AVenhance.Infra.Section5.H1Reduction.transfer_real_pullback_norm_le (G : C(UnitAddTorus (Fin 2), ℂ)) : ‖Heat.frozenCellToTorusL2 ⋯‖ ≤ ‖(ContinuousMap.toLp 2 MeasureTheory.volume ℂ) G‖

theorem AVenhance.Infra.Section5.H1Reduction.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.Section5.H1Reduction.value_norm {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ‖Heat.frozenCellToTorusL2 hf‖ = √(l2NormSq f)

theorem AVenhance.Infra.Section5.realHeatApprox_meanZero {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) {s : ℝ} (hs : 0 < s) : Homogenization.MeanZeroOn unitCube (realHeatApprox hf hs)

Heat evolution preserves the mean-zero condition.

def AVenhance.Infra.Section5.H1Reduction.tupleIndex {n : ℕ} (i : Fin n → Fin 2) (a : Fin 2) : ℕ

Multiplicity of a coordinate index in an ordered tuple of derivative directions.

Equations

• AVenhance.Infra.Section5.H1Reduction.tupleIndex i a = Fintype.card { j : Fin n // i j = a }

theorem AVenhance.Infra.Section5.H1Reduction.tupleIndex_degree {n : ℕ} (i : Fin n → Fin 2) : Heat.multiIndexDegree (tupleIndex i) = n

theorem AVenhance.Infra.Section5.H1Reduction.tupleIndex_factor {n : ℕ} (i : Fin n → Fin 2) (k : Heat.Frequency) : (2 * ↑Real.pi * Complex.I) ^ n * ↑(∏ j : Fin n, (Heat.frequencyPhaseCLM k) (Homogenization.basisVec (i j))) = Heat.multiIndexFourierFactor (tupleIndex i) k

theorem AVenhance.Infra.Section5.H1Reduction.realHeatApprox_derivative_eq {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) (n : ℕ) (i : Fin n → Fin 2) (x : Homogenization.Vec 2) : ((iteratedFDeriv ℝ n (realHeatApprox hf hs) x) fun (j : Fin n) => Homogenization.basisVec (i j)) = ((Heat.heatDerivativeTorusContinuous hs (Heat.frozenPeriodicH1ValueL2 hf) (tupleIndex i)) (Torus.toUnitTorus 2 x)).re

theorem AVenhance.Infra.Section5.realHeatApprox_derivative_bound {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) (n : ℕ) (i : Fin n → Fin 2) : √(∫ (x : Homogenization.Vec 2) in unitCube, ((iteratedFDeriv ℝ n (realHeatApprox hf hs) x) fun (j : Fin n) => Homogenization.basisVec (i j)) ^ 2) ≤ ↑n.factorial * (1 / √s) ^ n * √(l2NormSq f)

The real heat approximation satisfies the ordered-coordinate derivative bound.

noncomputable def AVenhance.Infra.Section5.datumLength (f : Homogenization.Vec 2 → ℝ) (Df : Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ

The gradient-only length scale, including the total value at zero data.

Equations

• AVenhance.Infra.Section5.datumLength f Df = √(AVenhance.l2NormSq f) / √(AVenhance.gradNormSq Df)

theorem AVenhance.Infra.Section5.H1Reduction.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.Section5.H1Reduction.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 < datumLength f Df

theorem AVenhance.Infra.Section5.H1Reduction.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) : datumLength f Df ^ 2 * gradNormSq Df = l2NormSq f

theorem AVenhance.Infra.Section5.H1Reduction.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.Section5.analytic_approximation {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 (α * datumLength f Df / 2) g ∧ l2NormSq (f - g) ≤ α ^ 2 * l2NormSq f ∧ l2NormSq f / 4 ≤ l2NormSq g

Heat smoothing produces an actual analytic datum and closes the distance estimate.

noncomputable def AVenhance.Infra.Section5.reductionAlpha (c p L : ℝ) : ℝ

Explicit smoothing parameter; p is the exponent of the squared energy.

Equations

• AVenhance.Infra.Section5.reductionAlpha c p L = min (1 / 4) ((c * (L / 2) ^ p / 32) ^ (1 / (2 - p)))

theorem AVenhance.Infra.Section5.H1Reduction.reductionAlpha_pos {c p L : ℝ} (hc : 0 < c) (hL : 0 < L) : 0 < reductionAlpha c p L

theorem AVenhance.Infra.Section5.H1Reduction.reductionAlpha_small {c p L : ℝ} (hc : 0 < c) (hp : p < 2) (hL : 0 < L) : reductionAlpha c p L ^ 2 ≤ c * (reductionAlpha c p L * L / 2) ^ p / 32

noncomputable def AVenhance.Infra.Section5.reductionRho (c p L : ℝ) : ℝ

Total positive dissipation coefficient, capped at one as required by the H¹ reduction.

Equations

• AVenhance.Infra.Section5.reductionRho c p L = if 0 < L then min 1 √(c * (AVenhance.Infra.Section5.reductionAlpha c p L * L / 2) ^ p / 16) else 1

theorem AVenhance.Infra.Section5.reductionRho_bounds {c p : ℝ} (hc : 0 < c) (L : ℝ) : 0 < reductionRho c p L ∧ reductionRho c p L ≤ 1

def AVenhance.Infra.Section5.AnalyticDissipationInput (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (c p : ℝ) : Prop

Analytic-case input H1, using the literal analytic and solution carriers. The exponent p acts on energy and is supplied by the §5.4 estimate.

Equations

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

def AVenhance.Infra.Section5.DifferenceEnergyInput (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

H2: the endpoint energy identity for the difference of two weak solutions.

Equations

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

def AVenhance.Infra.Section5.WeakWellposedInput (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

The weak well-posedness conclusion, copied literally, as a conditional data input. Existence is necessary to instantiate H1; H1 alone could otherwise be vacuous.

Equations

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

theorem AVenhance.Infra.Section5.H1Reduction.zero_solution (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) : IsWeakSolutionGrad b κ (fun (x : Homogenization.Vec 2) => 0) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.H1Reduction.zero_datum_memL2 : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.H1Reduction.st_integrable {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (D p.1 p.2)) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section5.H1Reduction.square_triangle (u v : ℝ) : v ^ 2 ≤ 2 * u ^ 2 + 2 * (u - v) ^ 2

theorem AVenhance.Infra.Section5.H1Reduction.st_triangle {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hE : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => E p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : spaceTimeGradNormSq E ≤ 2 * spaceTimeGradNormSq D + 2 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => D t x - E t x

theorem AVenhance.Infra.Section5.H1Reduction.energy_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hEnergy : DifferenceEnergyInput b) {κ : ℝ} (hκ : 0 < κ) {f : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Homogenization.MemL2On unitCube f) (hθ : IsWeakSolutionGrad b κ f θ D) : 0 ≤ κ * spaceTimeGradNormSq D ∧ κ * spaceTimeGradNormSq D ≤ l2NormSq f / 2

theorem AVenhance.Infra.Section5.H1Reduction.energy_comparison {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hEnergy : DifferenceEnergyInput b) {κ : ℝ} (hκ : 0 < κ) {f g : Homogenization.Vec 2 → ℝ} {θ η : ℝ → Homogenization.Vec 2 → ℝ} {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) (hθ : IsWeakSolutionGrad b κ f θ D) (hη : IsWeakSolutionGrad b κ g η E) : κ * spaceTimeGradNormSq E ≤ 2 * (κ * spaceTimeGradNormSq D) + l2NormSq (f - g)

theorem AVenhance.Infra.Section5.H1Reduction.limsup_transfer {ι : Type u_1} {F : Filter ι} [F.NeBot] {u v : ι → ℝ} {B E : ℝ} (hu : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) F u) (hv : ∀ᶠ (i : ι) in F, 0 ≤ v i) (hcmp : ∀ᶠ (i : ι) in F, v i ≤ 2 * u i + E) (hB : B ≤ Filter.limsup v F) : (B - E) / 2 ≤ Filter.limsup u F

theorem AVenhance.Infra.Section5.H1Reduction.variance_transfer {M A G E U : ℝ} (hM : 0 ≤ M) (hA : 0 ≤ A) (hG : A / 4 ≤ G) (hE : E ≤ M * A / 32) (hU : (M * G - E) / 2 ≤ U) : M / 16 * A ≤ U

theorem AVenhance.Infra.Section5.h1_dissipation_conditional {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c p : ℝ} (hc : 0 < c) (hp : 0 < p ∧ p < 2) (hWP : WeakWellposedInput b) (hAnalytic : AnalyticDissipationInput b c p) (hEnergy : DifferenceEnergyInput b) {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hθ : ∀ (κ : ℝ), 0 < κ → IsWeakSolutionGrad b κ f (θ κ) (Dθ κ)) : reductionRho c p (datumLength f Df) ^ 2 * l2NormSq f ≤ Filter.limsup (fun (κ : ℝ) => κ * spaceTimeGradNormSq (Dθ κ)) (nhdsWithin 0 (Set.Ioi 0))

Conditional reduction for a given general H1 datum and solution family. No solution existence, analytic dissipation, or difference energy is proved here.

theorem AVenhance.Infra.Section5.h1_reduction_conditional {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c p : ℝ} (hc : 0 < c) (hp : 0 < p ∧ p < 2) (hWP : WeakWellposedInput b) (hAnalytic : AnalyticDissipationInput b c p) (hEnergy : DifferenceEnergyInput b) : ∃ (ϱ : ℝ → ℝ), (∀ (L : ℝ), 0 < ϱ L ∧ ϱ L ≤ 1) ∧ ∀ (f : Homogenization.Vec 2 → ℝ) (Df : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With f Df → Homogenization.MeanZeroOn unitCube f → ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), (∀ (κ : ℝ), 0 < κ → IsWeakSolutionGrad b κ f (θ κ) (Dθ κ)) → ϱ (datumLength f Df) ^ 2 * l2NormSq f ≤ Filter.limsup (fun (κ : ℝ) => κ * spaceTimeGradNormSq (Dθ κ)) (nhdsWithin 0 (Set.Ioi 0))

Conclusion of the H¹ reduction: a single explicit positive rho depending only on the ratio L, with all analytic/PDE inputs exposed.