LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.Canonical

source

theorem HCPolySupport.coarseCaccioppoliBoundaryRadiusEnergyAnalyticInputs_at_pair {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) {lam Lam : ℝ} (F : ℝ → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (g : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) {ρ₁ ρ₂ : ℝ} (hρ₁ : 1 / 3 ≤ ρ₁) (hlt : ρ₁ < ρ₂) (_hρ₂ : ρ₂ ≤ 1) (hlower : F ρ₁ ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (houter : ρ₂ < 1) (henergyAvg : (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂) (hfluxMem : MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q)) (huMem : MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q)) (hgMem : MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (hscalar : CoarseCaccioppoliScalarCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C) (_hC : 0 ≤ C) (hAcirc1_nonneg : 0 ≤ Acirc1 ρ₁ ρ₂) (hAcircS_nonneg : 0 ≤ AcircS ρ₁ ρ₂) (hU : (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂) (hA1 : Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂) (hAS : AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂) :

F ρ₁ ≤ |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) ((w ρ₁ ρ₂).toH1.toFun x • scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x)| ∧ (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂ ∧ MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q) ∧ MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q) ∧ MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q) ∧ MeasureTheory.MemLp (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) ⊤ (normalizedCubeMeasure Q) ∧ (CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) ∧ CoarseCaccioppoliScalarCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C ∧ 0 ≤ coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂ ∧ 0 ≤ Acirc1 ρ₁ ρ₂ ∧ 0 ≤ AcircS ρ₁ ρ₂ ∧ (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂ ∧ cubeLpNorm Q ⊤ (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) ≤ coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂ ∧ coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂ ≤ coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂ ∧ Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂ ∧ AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂

Canonical-cutoff harmonic analytic inputs with the scalar cutoff package bundled as CoarseCaccioppoliScalarCutoffControls.

source

Canonical-cutoff harmonic analytic inputs at the concrete Chapter-3 radius sequence pair (ρ_n, ρ_{n+1}), with the strict outer-radius hypothesis discharged by the sequence itself.

source

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_scalarCutoffControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) {lam Lam : ℝ} (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (g : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hlower : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (houter : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ρ₂ < 1) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂) (hfluxMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q)) (huMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q)) (hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (hfluxEnergy : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (hscalar : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliScalarCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C) (hC : 0 ≤ C) (hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂) (hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ AcircS ρ₁ ρ₂) (hU : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂) (hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂) (hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂) :

CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C k h F (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) g (fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS

Canonical-cutoff harmonic analytic inputs with the scalar cutoff package bundled as CoarseCaccioppoliScalarCutoffControls.

source

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs.of_cutoff_coefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (flux : ℝ → ℝ → Vec d → Vec d) (u g energy : ℝ → ℝ → Vec d → ℝ) (η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂) (Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ) (htest : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ |cubeAverage Q fun (x : Vec d) => vecDot (flux ρ₁ ρ₂ x) (u ρ₁ ρ₂ x • scalarCutoffGradientField (η ρ₁ ρ₂).toFun x)|) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeAverage Q (energy ρ₁ ρ₂) = F ρ₂) (hfluxMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (flux ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (huMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (u ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (hfluxEnergy : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (flux ρ₁ ρ₂) (energy ρ₁ ρ₂)) (hBgConst : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ coarseCaccioppoliConstantCutoffSize Q (u ρ₁ ρ₂) (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂)) (hBgCent : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂) (√(cubeAverage Q (energy ρ₁ ρ₂))) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C) (hC : 0 ≤ C) (hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂) (hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ AcircS ρ₁ ρ₂) (hproj : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q (u ρ₁ ρ₂)) (g ρ₁ ρ₂) N) (hgCirc1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂))) (hgCircS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂))) (hU : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeLpNorm Q 2 (u ρ₁ ρ₂) ≤ U ρ₁ ρ₂) (hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂) (hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq k h U (coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS) :

CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F flux u g (fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (η ρ₁ ρ₂).toFun) energy Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS

Quantitative cutoff analytic inputs combine with the separated canonical coefficient algebra to produce the full canonical factor inputs.

source

theorem HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs.of_familyCoefficientBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) {lam Lam : ℝ} (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (g : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hlower : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ cubeAverage Q fun (x : Vec d) => QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (houter : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ρ₂ < 1) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂) (hfluxMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q)) (huMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q)) (hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q)) (hfluxEnergy : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (hscalar : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliScalarCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C) (hC : 0 ≤ C) (hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂) (hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ AcircS ρ₁ ρ₂) (hU : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂) (hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂) (hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂) (hcoeff : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq k h U (coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS) :

CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq k h F (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) g (fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS

Canonical Chapter-3 cutoff constructor for the full radius-indexed canonical factor-input package.

This is the direct handoff from the actual smooth cutoff QuantitativeCubeCutoff.canonicalFun: its L∞ and derivative bounds fill the Xi and D slots, while the remaining scalar-control and coefficient inequalities stay explicit.

Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.Canonical

Coarse-graining support: #