InteriorComposedArith

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Arithmetic for the interior-clause composition

Square roots, 3-powers and s-powers only. Nothing here has analytic content: every statement is an identity or an elementary inequality between explicit real expressions, isolated from the composition so that the assembly itself stays readable.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingForceTerm_le_of_seminorm_bounds {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) (r s : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) {b scale child parent : ℝ} (hb : 0 ≤ b) (hscale : 0 ≤ scale) (hbracket : coarseGrainingForceBracket Q a a0 r ≤ b) (hnonneg : 0 ≤ HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q s f) (hbesov : HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q s f ≤ scale * child) (hchild : child ≤ parent) : coarseGrainingForceTerm Q a a0 r s f ≤ b * (scale * parent)

Compare the forcing term through separate bracket and seminorm bounds. The coefficient family and comparator are arbitrary.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovScaleWeight_one_originCube {d : ℕ} (n : ℤ) : HCPolySupport.cubeBesovScaleWeight 1 (HCPolySupport.originCube d n) = Real.rpow 3 (-↑n)

The scale-one Besov weight on an origin cube.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalar_frame_main_le (A cap E sig R P QS Qf Q1 S4 T factor X Y : ℝ) (hA : 0 ≤ A) (hE : 0 ≤ E) (hcap : E ≤ cap) (hX : 0 ≤ X) (hY : 0 ≤ Y) (hQS : 0 ≤ QS) (hQf : 0 ≤ Qf) (hR : 0 ≤ R) (hS4 : 0 ≤ S4) (hinv : 0 ≤ sig⁻¹) (hcancel : sig⁻¹ * sig = 1) (hRP : R * P ≤ 1) (hforce : R * Qf ≤ factor * Q1) (hproduct : S4 * QS = T) : A * (sig⁻¹ * R * S4 * E * (sig * (P * X) + QS * (Qf * Y))) ≤ A * (S4 * E * X) + factor * cap * A * (T * sig⁻¹ * Q1 * Y)

A frame comparison separates the normalized energy and forcing legs.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalar_frame_decay_le (A sig R Q Q1 decay T Y : ℝ) (hA : 0 ≤ A) (hinv : 0 ≤ sig⁻¹) (hQ1 : 0 ≤ Q1) (hY : 0 ≤ Y) (hdecay : decay ≤ T) (hframe : R * Q = Q1) : A * (sig⁻¹ * R * decay * Q * Y) ≤ A * (T * sig⁻¹ * Q1 * Y)

A dominated decay factor controls a frame-normalized forcing term.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalar_frame_three_term_bounds (A1 A2 A3 cap E sig R P QS Qf Qshift Q1 S4 T sixth half factor X Y : ℝ) (hA1 : 0 ≤ A1) (hA2 : 0 ≤ A2) (hA3 : 0 ≤ A3) (hE : 0 ≤ E) (hcap : E ≤ cap) (hX : 0 ≤ X) (hY : 0 ≤ Y) (hQS : 0 ≤ QS) (hQf : 0 ≤ Qf) (hQ1 : 0 ≤ Q1) (hR : 0 ≤ R) (hS4 : 0 ≤ S4) (hT : 0 ≤ T) (hinv : 0 ≤ sig⁻¹) (hcancel : sig⁻¹ * sig = 1) (hRP : R * P ≤ 1) (hforce : R * Qf ≤ factor * Q1) (hframe : R * Qshift = Q1) (hproduct : S4 * QS = T) (hsixth : sixth ≤ T) (hhalf : half ≤ T) (hfactor : 0 ≤ factor) : A1 * (sig⁻¹ * R * S4 * E * (sig * (P * X) + QS * (Qf * Y))) ≤ A1 * (S4 * E * X) + factor * cap * A1 * (T * sig⁻¹ * Q1 * Y) ∧ A2 * (sig⁻¹ * R * sixth * Qshift * Y) ≤ A2 * (T * sig⁻¹ * Q1 * Y) ∧ A3 * (sig⁻¹ * R * half * Qshift * Y) ≤ A3 * (T * sig⁻¹ * Q1 * Y) ∧ 0 ≤ S4 * E * X ∧ 0 ≤ T * sig⁻¹ * Q1 * Y ∧ 0 ≤ factor * cap * A1

Product and domination identities assemble the three scalar comparison legs, independently of the exponents used to obtain those identities.

1. Square roots of powers

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_rpow_two_mul {b : ℝ} (hb : 0 < b) (y : ℝ) : √(b.rpow (2 * y)) = b.rpow y

√(b^{2y}) = b^y for a positive base.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_add_le_sqrt_add_sqrt {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) : √(A + B) ≤ √A + √B

Subadditivity of the square root.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_mul_sqrt_inv {a : ℝ} (ha : 0 < a) : √a * √a⁻¹ = 1

√a · √(a⁻¹) = 1 for a > 0.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_scalar_anchor_energy_le (sig s t exponent X Y : ℝ) (hsig : 0 < sig) (hs : 0 < s) (hX : 0 ≤ X) (hY : 0 ≤ Y) : √(sig * Real.rpow 3 (-2 * t) * X ^ 2 + s.rpow exponent * sig⁻¹ * Real.rpow 3 (2 * s * t) * Y ^ 2) ≤ √sig * Real.rpow 3 (-t) * X + s.rpow (exponent / 2) * √sig⁻¹ * Real.rpow 3 (s * t) * Y

The two scalar energy legs, for any positive diffusivity and real forcing exponent.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_interiorAnchorEnergyRHSOn_le {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {s : ℝ} (hs : 0 < s) (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : √(interiorAnchorEnergyRHSOn M n s W f g) ≤ √↑(Section3.Annealed.sigmaBar M (n + 2)) * Real.rpow 3 (-↑(n + 2)) * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverage W f) 2 (Support.normalizedVolumeMeasureOn W)).toReal + s.rpow (-(11 / 2)) * √(↑(Section3.Annealed.sigmaBar M (n + 2)))⁻¹ * Real.rpow 3 (s * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn W s g).toReal

The two legs of the interior-Caccioppoli right-hand side.

  ( σ 3^{-2(n+2)} X² + s^{-11} σ^{-1} 3^{2s(n+2)} Y² )^{1/2}
      ≤ σ^{1/2} 3^{-(n+2)} X  +  s^{-11/2} σ^{-1/2} 3^{s(n+2)} Y .

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantCoeffMatrixNormHalf_scalarComparator_sqrt {d : ℕ} [NeZero d] {sigma : ℝ} (hsigma : 0 < sigma) : HCPolySupport.Book.Ch03.constantCoeffMatrixNormHalf (scalarComparator hsigma) = √sigma

The comparator's half-norm, in the Real.sqrt spelling.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGraining_comparisonBounds {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {sig : ℝ} (hsig : 0 < sig) (r kappa Erep Eb e0 Cout P QS Qf X Y : ℝ) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (hkappa : 0 ≤ kappa) (hErep : 0 ≤ Erep) (hEb : 0 ≤ Eb) (hEbe0 : Eb ≤ e0) (herr : HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth Q a (scalarComparator hsig) r 0 ≤ kappa * Erep) (hbracket : coarseGrainingForceBracket Q a (scalarComparator hsig) r ≤ √(2 * ↑d * (Eb ^ 2 + 1)) * Eb + 2 * (2 * ↑d * (Eb ^ 2 + 1))) (hEnergy : HCPolySupport.Book.Ch03.h1EnergyNormOnCube Q a u ≤ √Cout * (√sig * P * X + QS * √sig⁻¹ * Qf * Y)) : have k0 := 2 * ↑d * (e0 ^ 2 + 1); coarseGrainingForceBracket Q a (scalarComparator hsig) r ≤ √k0 * e0 + 2 * k0 ∧ coarseGrainingEnergyTerm Q a (scalarComparator hsig) r u ≤ kappa * √Cout * Erep * (sig * (P * X) + QS * (Qf * Y))

Error and energy bounds control both coarse-graining comparison coefficients.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.besovVectorSeminormTwo_originCube_translated_neg_le {d : ℕ} [NeZero d] {x : HCPolySupport.Vec d} (n : ℤ) {s : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hs : 0 < s) (hs1 : s ≤ 1) (hL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d n) s fun (y : HCPolySupport.Vec d) => -g (y + x)) ≤ besovGagliardoConstant d * Real.rpow 3 (s * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s g).toReal

The translated Besov estimate with its origin-cube scale weight evaluated.

3. The 3-powers of the frame division

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_three_neg_mul_self (n : ℤ) : Real.rpow 3 (-↑n) * Real.rpow 3 ↑n = 1

Dividing by the left-hand weight 3^{-n} is multiplying by 3^{n}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_three_frame_l2_le_one (n : ℤ) : Real.rpow 3 ↑n * Real.rpow 3 (-↑(n + 2)) ≤ 1

The L² leg's scale weights: 3^{n} · 3^{-(n+2)} ≤ 1.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_three_frame_force_le (n : ℤ) {s : ℝ} (hs1 : s ≤ 1) : Real.rpow 3 ↑n * Real.rpow 3 (s * ↑(n + 2)) ≤ 9 * Real.rpow 3 ((1 + s) * ↑n)

The forcing leg's scale weights: 3^{n} · 3^{s(n+2)} ≤ 9 · 3^{(1+s)n}.

4. The s-powers of the composition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.inv_pow_eq_rpow_neg {s : ℝ} (hs : 0 < s) (k : ℕ) : s⁻¹ ^ k = s.rpow (-↑k)

(s⁻¹)^k = s^{-k} for positive s and a natural exponent.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_s_four_mul_eleven_halves {s : ℝ} (hs : 0 < s) : s.rpow (-4) * s.rpow (-(11 / 2)) = s.rpow (-(19 / 2))

The two s-powers of the composition add: s^{-4} · s^{-11/2} = s^{-19/2}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_le_rpow_neg_nineteen_halves {s a : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (ha : -(19 / 2) ≤ a) : s.rpow a ≤ s.rpow (-(19 / 2))

On (0,1] every s-power above −19/2 is dominated by s^{-19/2}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.comparison_constants_nonneg (d : ℕ) [NeZero d] (CE energyFactor windowFactor : ℝ) (hCE : 0 ≤ CE) (henergy : 0 ≤ energyFactor) (hwindow : 0 ≤ windowFactor) : have kappa := √(192 * ↑d) * 3; have e0 := kappa * (CE * (1 / 2)); have k0 := 2 * ↑d * (e0 ^ 2 + 1); have b0 := √k0 * e0 + 2 * k0; have cg := 3 * negNormBaseConst d * coarseGrainingP2Const d; have A1 := cg * 216 * (kappa * energyFactor); have A2 := cg * 1944 * (b0 * (besovGagliardoConstant d * windowFactor)); have A3 := interiorCorrectionConst d * windowFactor; 0 ≤ kappa ∧ 0 ≤ b0 ∧ 0 ≤ cg ∧ 0 ≤ A1 ∧ 0 ≤ A2 ∧ 0 ≤ A3 ∧ 0 ≤ 9 * (CE * (1 / 2)) * A1 ∧ 0 ≤ CE * (1 / 2) * A1

Nonnegativity of composed constants for supplied energy and window factors.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.composed_constants_nonneg (d : ℕ) [NeZero d] (CE Cout : ℝ) (hCE : 0 ≤ CE) : have kappa := √(192 * ↑d) * 3; have e0 := kappa * (CE * (1 / 2)); have k0 := 2 * ↑d * (e0 ^ 2 + 1); have b0 := √k0 * e0 + 2 * k0; have cg := 3 * negNormBaseConst d * coarseGrainingP2Const d; have A1 := cg * 216 * (kappa * √Cout); have A2 := cg * 1944 * (b0 * (besovGagliardoConstant d * gagliardoWindowConst d)); have A3 := interiorCorrectionConst d * gagliardoWindowConst d; 0 ≤ kappa ∧ 0 ≤ b0 ∧ 0 ≤ cg ∧ 0 ≤ A1 ∧ 0 ≤ A2 ∧ 0 ≤ A3

Positivity of the common constants in the two composed scale estimates.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalar_frame_cancel_le {sig P R lhs rhs : ℝ} (hsig : 0 < sig) (hR : 0 ≤ R) (hPR : P * R = 1) (h : sig * (P * lhs) ≤ rhs) : lhs ≤ sig⁻¹ * R * rhs

Cancel a positive scalar and an inverse pair of frame weights.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.three_leg_comparison_close {w cg a b c energy forcing child E F Y A1 B A2 A3 X Z lhs : ℝ} (hw : 0 ≤ w) (hcg : 0 ≤ cg) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (henergy : energy ≤ E) (hforcing : forcing ≤ F) (hchild : child ≤ Y) (hstep : lhs ≤ w * (cg * (a * energy + b * forcing) + c * child)) (hfirst : w * (cg * (a * E)) ≤ A1 * X + B * Z) (hsecond : w * (cg * (b * F)) ≤ A2 * Z) (hthird : w * (c * Y) ≤ A3 * Z) (hA1 : 0 ≤ A1) (hB : 0 ≤ B) (hA2 : 0 ≤ A2) (hA3 : 0 ≤ A3) (hX : 0 ≤ X) (hZ : 0 ≤ Z) : lhs ≤ (A1 + B + A2 + A3 + 1) * (X + Z)

Replace three comparison legs and collect their two nonnegative output quantities.