Big-bound estimate wiring: BigBoundStatement from the explicit §5.2 inputs

bigbound_of_inputs turns the conditional §5.2 term estimates (Terms/*Scale.lean) and the conditional ten-term assembly into the literal big-bound estimate proposition BigBoundStatement β C₀. The inputs proved in other modules are collected, for one instance, in the Prop-valued structure BigBoundInputs; no field is (or contains) the big-bound estimate conclusion.

Hypotheses of the existing conditional lemmas that are derived here and therefore not fields:

• MemL2On of every slice of every term and the time measurability of the HDot⁻¹ norms of the terms and of all partial sums (from joint continuity term_continuous, via HMinusMeasurable.lean);
• the residual identity at closed times / all x (only open times Ioo 0 1 are used, timeHMinusOneNorm_residual_le_sum_sourceScale_Ioo);

Grouped mean zero: the assembly uses that the sum of twistie4, twistie5 and normie3 is mean zero (group_meanZero). It runs on the centered ten-term family section5CenteredTerm (slots 3, 4, 8 replaced by centerCell, see BigBound/Grouped.lean), whose pointwise sum equals the original ten-term sum on (0,1) by group_meanZero. The three centered slots are bounded directly by the fields twistie4_centered_source, twistie5_centered_source, normie3_centered_source; the other seven slots by the existing conditional *_sourceScale theorems.

Small analytic and ENNReal helpers

theorem AVenhance.Infra.Section5.Integration.ofReal_rpow_neg_half_mul_sum_ten {κ : ℝ} (hκ : 0 < κ) (c : ℝ) : ENNReal.ofReal (κ ^ (-(1 / 2))) * ∑ _i ∈ Finset.range 10, ENNReal.ofReal (c * √κ) = ENNReal.ofReal (10 * c)

ofReal (κ ^ (-1/2)) times the sum of ten copies of ofReal (c √κ) is ofReal (10 c).

theorem AVenhance.Infra.Section5.Integration.timeHMinusOneNorm_le_of_bigbound_conclusion {κm X : ℝ} {N : ENNReal} (h : ENNReal.ofReal (κm ^ (-(1 / 2))) * N ≤ ENNReal.ofReal X) (hκ : 0 < κm) : N ≤ ENNReal.ofReal (X * √κm)

Conversion of the normalised (κ_m ^ (-1/2)) bound to the plain time-norm bound used in the κ_m^{1/2}-scaled form (step-down part (i)).

The ten-term assembly with the residual identity on open times only

theorem AVenhance.Infra.Section5.Integration.timeHMinusOneNorm_residual_le_sum_sourceScale_Ioo {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hResidual : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), residualIdentity I hΦ m κm T d e b t x) (htermL2 : ∀ i < 10, ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (section5Term I hΦ m κm T d e i t)) (htermMeas : ∀ i < 10, AEMeasurable (fun (t : ℝ) => hMinusOneNorm (section5Term I hΦ m κm T d e i t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hprefixMeas : ∀ (n : ℕ), 1 ≤ n → n < 10 → AEMeasurable (fun (t : ℝ) => hMinusOneNorm (section5Prefix I hΦ m κm T d e n t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) {S : ℝ} (htermScale : ∀ i < 10, timeHMinusOneNorm (section5Term I hΦ m κm T d e i) ≤ ENNReal.ofReal S) : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp b κm (I.ansatz hΦ m κm T) t x) ≤ ∑ _i ∈ Finset.range 10, ENNReal.ofReal S

timeHMinusOneNorm_residual_le_sum_sourceScale, with the residual identity assumed only for t ∈ (0,1) (the only times seen by the time norm).

The input structure

structure AVenhance.Infra.Section5.Integration.BigBoundInputs {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (C : ℝ) : Prop

The remaining upstream statements needed to obtain the big-bound estimate bound e.bigbound for ONE instance (I, Φ, m, κ_m, κ_{m-1}, T, θ₀) with common constant C.

Notation: N := T (Nstar β) is the final T-iterate, d := sourceErrorD I hΦ m κm N, e := iterateError I hΦ m κm κprev T, S := section5SourceScale β I.Λ m κm C θ₀ = C ε_{m-1}^δ √κ_m ‖θ₀‖. The hsource fields are the S-sized space-time L² bounds on the spatial L² norm (or flux gradient norm) of each term (the "monster" display e.monster.cutoff1–e.monster.normie3, enhance.tex 6886–6990; estimates 7300–8010).

Grouped mean zero: twistie4, twistie5, normie3 carry no individual mean-zero or source field; instead group_meanZero (their sum is mean zero) and the three centered negative-norm bounds twistie4_centered_source, twistie5_centered_source, normie3_centered_source.

Fields dropped relative to the underlying conditional lemmas (proved in this file, from the single field term_continuous): MemL2On of every slice of every term (memL2On_of_continuousOn_slice), the time measurability of the HDot⁻¹ norm of every term and every partial sum (aemeasurable_hMinusOneNorm_of_continuousOn; a partial sum of continuous terms is continuous), the residual identity at t ∉ (0,1).

• residual : ResidualContract I hΦ m κm κprev T

  The exact ε-residual identity e.monster for the ansatz built from N = T (Nstar β) with the source errors d_m (e.dm) and e_{m-1} (enhance.tex 6886–6990).

• cutoff1_meanZero : Cutoff1MeanZeroContract I hΦ m κm T

  Mean zero of cutoff1(t) on the cube, t ∈ (0,1).

• cutoff1_source : Cutoff1SourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Source-scale space-time L² bound for cutoff1 (e.monster.est.*, 7300–7500; a §3/§4 bound).

• twistie1_hminus_source : Twistie1HMinusSourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Negative-norm source bound for twistie1 (e.monster.est.5, ergodic lemma).

• twistie3_flux_smooth : Twistie3FluxSmoothContract I hΦ m κm T

  Smoothness of the divergence flux of twistie3 (e.monster.twistie3, 6912), t ∈ (0,1).

• twistie3_flux_periodic : Twistie3FluxPeriodicContract I hΦ m κm T

  ℤ²-periodicity of the twistie3 flux.

• twistie3_source : Twistie3SourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Source-scale space-time L² bound on ∇ (twistie3 flux)-norm (§3/§4 bound).

• group_meanZero : GroupMeanZeroContract I hΦ m κm T

  Grouped mean zero: the sum of twistie4, twistie5 and normie3 is mean zero on the cube for t ∈ (0,1); the centered estimates below use this grouped form.

• twistie4_centered_source : Twistie4CenteredSourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Centered negative-norm bound for twistie4: the time HDot⁻¹ norm of its unit-cube centering is at most the common source scale.

• twistie5_centered_source : Twistie5CenteredSourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Centered negative-norm bound for twistie5.

• normie3_centered_source : Normie3CenteredSourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Centered negative-norm bound for normie3.

• normie1_flux_smooth : Normie1FluxSmoothContract I hΦ m κm T

  Smoothness of the divergence flux of normie1 (e.monster.normie1, 6950).

• normie1_flux_periodic : Normie1FluxPeriodicContract I hΦ m κm T

  ℤ²-periodicity of the normie1 flux.

• normie1_source : Normie1SourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Source-scale space-time L² bound on the normie1 flux gradient (§3/§4 bound).

• normie2_flux_smooth : Normie2FluxSmoothContract I hΦ m κm T

  Smoothness of the divergence flux of normie2 (e.monster.normie2, 6959).

• normie2_flux_periodic : Normie2FluxPeriodicContract I hΦ m κm T

  ℤ²-periodicity of the normie2 flux.

• normie2_source : Normie2SourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Source-scale space-time L² bound on the normie2 flux gradient (§3/§4 bound; H_m estimates).

• tiny_hminus_source : TinyHMinusSourceContract I hΦ m κm κprev T C √(l2NormSq θ₀)

  Negative-norm source bound for tiny (e.monster.est.tiny, divergence form).

• R46_flux_smooth : R46FluxSmoothContract I hΦ m κm T

  Smoothness of the transition-window flux of R46 (the transition remainder).

• R46_flux_periodic : R46FluxPeriodicContract I hΦ m κm T

  ℤ²-periodicity of the R46 flux.

• R46_source : R46SourceContract I hΦ m κm T C √(l2NormSq θ₀)

  Source-scale L² bound on the R46 flux gradient (the transition-window estimate that the source does not state; §3/§4 bound).

• term_continuous : TermContinuousContract I hΦ m κm κprev T

  Joint continuity of every named term on (0,1) × ℝ² (source: all pieces are smooth for t > 0). From it are derived the L² regularity of every slice t ∈ (0,1) and the time measurability of the HDot⁻¹ norms of the terms and of their partial sums.

theorem AVenhance.Infra.Section5.Integration.BigBoundInputs.termL2 {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {C : ℝ} (h : BigBoundInputs I hΦ m κm κprev T θ₀ C) (i : ℕ) : i < 10 → ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (section5Term I hΦ m κm (T (Nstar β)) (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) i t)

Every slice t ∈ (0,1) of every term is L² on the cube (continuity of the term).

theorem AVenhance.Infra.Section5.Integration.BigBoundInputs.centeredTerm_continuous {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {C : ℝ} (h : BigBoundInputs I hΦ m κm κprev T θ₀ C) (i : ℕ) : i < 10 → ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => section5CenteredTerm I hΦ m κm (T (Nstar β)) (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) i p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)

Every slot of the centered ten-term family is jointly continuous on (0,1) × ℝ² (centering preserves joint continuity).

theorem AVenhance.Infra.Section5.Integration.BigBoundInputs.centeredTermScale {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {C : ℝ} (h : BigBoundInputs I hΦ m κm κprev T θ₀ C) (i : ℕ) : i < 10 → timeHMinusOneNorm (section5CenteredTerm I hΦ m κm (T (Nstar β)) (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) i) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

The ten source-scale bounds for the centered family: the seven ungrouped slots by the existing conditional *_sourceScale theorems, the three grouped slots directly by the *_centered_source fields.

theorem AVenhance.Infra.Section5.Integration.BigBoundInputs.residual_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {C : ℝ} (h : BigBoundInputs I hΦ m κm κprev T θ₀ C) : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) κm (I.ansatz hΦ m κm (T (Nstar β))) t x) ≤ ∑ _i ∈ Finset.range 10, ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

The residual time norm is at most ten times the common source scale. The residual equals the ten-term sum, which on (0,1) equals the centered ten-term sum (group_meanZero); triangle inequality over the centered slots.

The big-bound estimate wiring theorem

def AVenhance.Infra.Section5.Integration.BigBoundFamilyContract (β C₀ : ℝ) : Prop

Family contract for big-bound estimate (IndyStepDownV2Inputs.bigbound): constants C₁ (Λ-threshold) and C₂ (common source constant) chosen before I, then BigBoundInputs on the big-bound premise block OnA7Instances. Each field of BigBoundInputs is produced separately as its *Contract.

Equations

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

theorem AVenhance.Infra.Section5.Integration.bigbound_of_inputs (β C₀ : ℝ) (hin : BigBoundFamilyContract β C₀) : BigBoundStatement β C₀

Big-bound estimate wiring. If, for every admissible instance with C₁ ≤ Λ, the explicit BigBoundInputs (the remaining §3/§4/§5 statements) hold with a constant C₂, then the Big-bound estimate proposition BigBoundStatement β C₀ holds with C = max C₁ (10 C₂).