Coarse-graining support: Support.CoarseGraining.BlockResponse.Equalities.MainEqualities

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

BlockResponse Equalities -- blockJ equals half-responseJ-adjoint-sum

blockJ le / eq half responseJ adjoint sum under IsEllipticFieldOn with hodgeConverseCriterion or IsOpenBoundedConvexDomain, together with the note-form variants.

theorem HCPolySupport.blockJ_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (hHodge : HodgeConverseCriterion U) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a ≤ 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_le_half_responseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a ≤ 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_note_le_half_adjointResponseSum_of_HodgeConverse {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (hHodge : HodgeConverseCriterion U) (p q h : Vec d) : BlockJ U (p, h) (q, 0) a ≤ 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a)

theorem HCPolySupport.blockJ_le_half_adjointResponseSum {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a ≤ 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_note_le_half_adjointResponseSum_of_ConvexDomain {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q h : Vec d) : BlockJ U (p, h) (q, 0) a ≤ 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a)

theorem HCPolySupport.half_responseJ_adjoint_sum_le_blockJ_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p pStar q qStar : Vec d) : 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a) ≤ BlockJ U (p, q) (qStar, pStar) a

theorem HCPolySupport.half_responseJ_adjoint_sum_note_form_le_blockJ_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q h : Vec d) : 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a) ≤ BlockJ U (p, h) (q, 0) a

theorem HCPolySupport.blockJ_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (hHodge : HodgeConverseCriterion U) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_note_form_eq_half_responseJ_adjoint_sum_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q h : Vec d) : BlockJ U (p, h) (q, 0) a = 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a)

theorem HCPolySupport.blockJ_note_eq_half_adjointResponseSum_of_HodgeConverse {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (hHodge : HodgeConverseCriterion U) (p q h : Vec d) : BlockJ U (p, h) (q, 0) a = 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a)

theorem HCPolySupport.blockJ_eq_half_adjointResponseSum_of_ConvexDomain {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p pStar q qStar : Vec d) : BlockJ U (p, q) (qStar, pStar) a = 1 / 2 * ResponseJ U (p - pStar) (qStar - q) a + 1 / 2 * ResponseJ U (pStar + p) (qStar + q) (adjointCoeffField a)

theorem HCPolySupport.blockJ_note_eq_half_adjointResponseSum_of_ConvexDomain {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q h : Vec d) : BlockJ U (p, h) (q, 0) a = 1 / 2 * ResponseJ U p (q - h) a + 1 / 2 * ResponseJ U p (q + h) (adjointCoeffField a)