Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.Basic

Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.Basic #

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

Basic scalar parameters for the third Section 5.3 lemma #

This file contains only the manuscript scalar parameters for l.J.upper.bound.coarse.fluctuations.homogenization.scale and the elementary inequalities extracted from (P4).

source
noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBetaCore {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
ℝ

The minimum quantity whose fixed small fraction is the exponent β in the third Section 5.3 lemma.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
    ℝ

    The exponent β used in l.J.upper.bound.coarse.fluctuations.homogenization.scale.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationZeta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
      ℝ

      The Hölder conjugate ζ = ξ / (ξ - 1) used in the third Section 5.3 lemma.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBetaCoreParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
        ℝ

        Parameter-only version of the Section 5.3 coarse-fluctuation beta core.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
          ℝ

          Parameter-only version of the Section 5.3 coarse-fluctuation beta.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationZetaParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) :
            ℝ

            Parameter-only version of the Section 5.3 Hölder conjugate exponent.

            Equations
            Instances For
              source
              @[simp]
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBetaCoreParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationBetaCoreParams hP4.params = section53CoarseFluctuationBetaCore hP4
              source
              @[simp]
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBetaParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              coarseFluctuationBeta hP4.params = section53CoarseFluctuationBeta hP4
              source
              @[simp]
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationZetaParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationZetaParams hP4.params = section53CoarseFluctuationZeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              0 < section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              0 ≤ section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_le_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationBeta hP4 ≤ hP4.sUpper
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_le_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationBeta hP4 ≤ hP4.sLower
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_le_sUpper_sub_dim_div_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationBeta hP4 ≤ hP4.sUpper - ↑d / ↑hP4.xi
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_le_sLower_sub_dim_div_xi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationBeta hP4 ≤ hP4.sLower - ↑d / ↑hP4.xi
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_sLower_add_two_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper + hP4.sLower + 2 * section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_sLower_add_four_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper + hP4.sLower + 4 * section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sLower_add_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sLower + section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sLower_add_two_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sLower + 2 * section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper + section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_two_beta_le_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper + 2 * section53CoarseFluctuationBeta hP4 ≤ 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.half_sLower_add_beta_le_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              (hP4.sLower + section53CoarseFluctuationBeta hP4) / 2 ≤ hP4.sLower
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sLower_lt_sLower_add_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sLower < hP4.sLower + section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.half_sLower_add_two_beta_le_sLower_add_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              (hP4.sLower + 2 * section53CoarseFluctuationBeta hP4) / 2 ≤ hP4.sLower + section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sLower_add_beta_lt_sLower_add_two_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sLower + section53CoarseFluctuationBeta hP4 < hP4.sLower + 2 * section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.half_sUpper_add_beta_le_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              (hP4.sUpper + section53CoarseFluctuationBeta hP4) / 2 ≤ hP4.sUpper
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_lt_sUpper_add_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper < hP4.sUpper + section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.half_sUpper_add_two_beta_le_sUpper_add_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              (hP4.sUpper + 2 * section53CoarseFluctuationBeta hP4) / 2 ≤ hP4.sUpper + section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_beta_lt_sUpper_add_two_beta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              hP4.sUpper + section53CoarseFluctuationBeta hP4 < hP4.sUpper + 2 * section53CoarseFluctuationBeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sLower_add_beta_sub_dim_div_xi_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              0 < hP4.sLower + section53CoarseFluctuationBeta hP4 - ↑d / ↑hP4.xi
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sUpper_add_beta_sub_dim_div_xi_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              0 < hP4.sUpper + section53CoarseFluctuationBeta hP4 - ↑d / ↑hP4.xi
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationZeta_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              0 < section53CoarseFluctuationZeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.one_lt_section53CoarseFluctuationZeta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              1 < section53CoarseFluctuationZeta hP4
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationZeta_le_two {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              section53CoarseFluctuationZeta hP4 ≤ 2
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.inv_xi_add_inv_section53CoarseFluctuationZeta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
              (↑hP4.xi)⁻¹ + (section53CoarseFluctuationZeta hP4)⁻¹ = 1
              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sq_sum_mul_sqrt_le_sum_mul_sum_mul {ι : Type u_1} (s : Finset ι) (w X : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hX : ∀ i ∈ s, 0 ≤ X i) :
              (∑ i ∈ s, w i * √(X i)) ^ 2 ≤ (∑ i ∈ s, w i) * ∑ i ∈ s, w i * X i

              Weighted finite Cauchy-Schwarz in the square-root form used by the expectation-level Section 5.3 RHS conversion.

              source
              theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.weighted_pair_sq_sum_mul_sqrt_le {ι : Type u_1} (s : Finset ι) (wg wf G F : ι → ℝ) {σ τ : ℝ} (hσ : 0 ≤ σ) (hτ : 0 ≤ τ) (hwg : ∀ i ∈ s, 0 ≤ wg i) (hwf : ∀ i ∈ s, 0 ≤ wf i) (hG : ∀ i ∈ s, 0 ≤ G i) (hF : ∀ i ∈ s, 0 ≤ F i) :
              σ * (∑ i ∈ s, wg i * √(G i)) ^ 2 + τ * (∑ i ∈ s, wf i * √(F i)) ^ 2 ≤ (∑ i ∈ s, wg i) * ∑ i ∈ s, wg i * (σ * G i) + (∑ i ∈ s, wf i) * ∑ i ∈ s, wf i * (τ * F i)

              Paired weighted finite Cauchy-Schwarz estimate, with separate scalar weights on the two components.