LayerPressure.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HenonLaneEmden.LayerPressure.components line 14
Source documentation
The actual (nonempty) connected components of an open real line layer.
```
def components (U : Set ℝ) : Set (Set ℝ) := connectedComponentIn U '' U
```
lemma OAI.HenonLaneEmden.LayerPressure.component_nonempty line 16
lemma OAI.HenonLaneEmden.LayerPressure.component_open line 20
lemma OAI.HenonLaneEmden.LayerPressure.component_connected line 24
lemma OAI.HenonLaneEmden.LayerPressure.component_identify line 28
lemma OAI.HenonLaneEmden.LayerPressure.components_disjoint line 33
lemma OAI.HenonLaneEmden.LayerPressure.components_countable line 40
lemma OAI.HenonLaneEmden.LayerPressure.biUnion_components line 44

lemma OAI.HenonLaneEmden.LayerPressure.lintegral_layer_comparison line 55

Source documentation

Nonnegative integration can be summed over two line-layer component families without any integrability or finiteness assumption on either side.

lemma lintegral_layer_comparison {U V : Set ℝ} (hU : IsOpen U) (hV : IsOpen V)
    (F G : ℝ × ℝ → ℝ≥0∞)
    (h : ∀ I ∈ components U, ∀ J ∈ components V,
      (∫⁻ z in I ×ˢ J, F z) ≤ ∫⁻ z in I ×ˢ J, G z) :
    (∫⁻ z in U ×ˢ V, F z) ≤ ∫⁻ z in U ×ˢ V, G z := by
…

Mentions: OAI.HenonLaneEmden.LayerPressure.components

lemma OAI.HenonLaneEmden.LayerPressure.open_connected_eq_Ioo line 91

lemma OAI.HenonLaneEmden.LayerPressure.component_pair_comparison line 107

Source documentation

The interval comparison stated directly on a product of two open components. The endpoint values on an unbounded component are immaterial because its weight is zero. All integrands are nonnegative extended values.

lemma component_pair_comparison (n : ℕ) (hn : 3 ≤ n)
    {I J : Set ℝ} (hopI : IsOpen I) (hopJ : IsOpen J)
    (hconI : IsConnected I) (hconJ : IsConnected J)
    {l C cI cJ : ℝ} (hl : 0 < l) (hC : 0 ≤ C) (hcI : 0 ≤ cI) (hcJ : 0 ≤ cJ)
    (hbI : 0 < cI → BddBelow I ∧ BddAbove I)
    (hbJ : 0 < cJ → BddBelow J ∧ BddAbove J) :
    (∫⁻ z in I ×ˢ J, ENNReal.ofReal ((cI+cJ)*kernel n l C (z.1-z.2))) ≤
    ∫⁻ z in I ×ˢ J, ENNReal.ofReal
      (cI*((kernel n l C (sInf I-z.2)+kernel n l C (sSup I-z.2))/2) +
       cJ*((kernel n l C (z.1-sInf J)+kernel n l C (z.1-sSup J))/2) +
       (((n:ℝ)-2)*min cI cJ*((z.1-z.2)^2/(l^2+(z.1-z.2)^2))+|cI-cJ|)*
         kernel n l C (z.1-z.2)) := by
…

lemma OAI.HenonLaneEmden.LayerPressure.open_layer_comparison line 159

Source documentation

Weighted interval comparison summed over two general open line layers. The coefficients are arbitrary nonnegative component-constant weights, with positive weight permitted only on bounded components.

lemma open_layer_comparison (n : ℕ) (hn : 3 ≤ n)
    {U V : Set ℝ} (hU : IsOpen U) (hV : IsOpen V)
    (c d : Set ℝ → ℝ) {l C : ℝ} (hl : 0 < l) (hC : 0 ≤ C)
    (hc : ∀ I ∈ components U, 0 ≤ c I) (hd : ∀ J ∈ components V, 0 ≤ d J)
    (hbc : ∀ I ∈ components U, 0 < c I → BddBelow I ∧ BddAbove I)
    (hbd : ∀ J ∈ components V, 0 < d J → BddBelow J ∧ BddAbove J) :
    (∫⁻ z in U ×ˢ V, ENNReal.ofReal
      ((c (connectedComponentIn U z.1)+d (connectedComponentIn V z.2))*kernel n l C (z.1-z.2))) ≤
    ∫⁻ z in U ×ˢ V, ENNReal.ofReal
      (c (connectedComponentIn U z.1)*
        ((kernel n l C (sInf (connectedComponentIn U z.1)-z.2)+
          kernel n l C (sSup (connectedComponentIn U z.1)-z.2))/2) +
…

Mentions: OAI.HenonLaneEmden.LayerPressure.components

def OAI.HenonLaneEmden.LayerPressure.lineWeight line 197
def OAI.HenonLaneEmden.LayerPressure.leftAverage line 200
def OAI.HenonLaneEmden.LayerPressure.rightAverage line 203
lemma OAI.HenonLaneEmden.LayerPressure.lineWeight_nonneg line 206
lemma OAI.HenonLaneEmden.LayerPressure.lineWeight_le line 209

lemma OAI.HenonLaneEmden.LayerPressure.weighted_source_layer_comparison line 218

Source documentation

The actual capped component weights satisfy the summed nonnegative layer comparison of equation (layer-pair), still before integrations over levels and transverse variables. No boundedness of either whole layer is assumed.

lemma weighted_source_layer_comparison (n : ℕ) (hn : 3 ≤ n)
    {U V : Set ℝ} (hU : IsOpen U) (hV : IsOpen V)
    (h₁ h₂ d₁ d₂ : ℝ → ℝ) (δ : ℝ) {l C : ℝ} (hl : 0 < l) (hC : 0 ≤ C)
    (hh₁ : ∀ x ∈ U, 0 ≤ h₁ x) :
    (∫⁻ z in U ×ˢ V, ENNReal.ofReal
      ((lineWeight U h₁ d₁ δ z.1+lineWeight V h₂ d₂ δ z.2)*kernel n l C (z.1-z.2))) ≤
    ∫⁻ z in U ×ˢ V, ENNReal.ofReal
      (lineWeight U h₁ d₁ δ z.1*leftAverage U (kernel n l C) z.1 z.2 +
       lineWeight V h₂ d₂ δ z.2*rightAverage V (kernel n l C) z.1 z.2 +
       (((n:ℝ)-2)*h₁ z.1*((z.1-z.2)^2/(l^2+(z.1-z.2)^2))+
         |lineWeight U h₁ d₁ δ z.1-lineWeight V h₂ d₂ δ z.2|)*kernel n l C (z.1-z.2)) := by
…

Mentions: OAI.HenonLaneEmden.LayerPressure.lineWeight, OAI.HenonLaneEmden.LayerPressure.leftAverage, OAI.HenonLaneEmden.LayerPressure.rightAverage