OAI/Analysis/HenonEmden/SphereCaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.CapWeights.lowerConstant line 18
2. def OAI.HenonLaneEmden.CapWeights.upperConstant line 20
3. lemma OAI.HenonLaneEmden.CapWeights.constants_positive line 23
4. lemma OAI.HenonLaneEmden.CapWeights.sphere_normalizer_bounds line 27
5. lemma OAI.HenonLaneEmden.CapWeights.sphere_normalizer_pos line 44
6. lemma OAI.HenonLaneEmden.CapWeights.sphere_normalized_oscillation line 49

   Source documentation

   Oscillation of a normalized cap with comparable radii, uniformly in directions.

   lemma sphere_normalized_oscillation
       {θ θ' : sphere (0:E) 1} {l l' ρ : ℝ} (hρ : 0 < ρ)
       (hl : ρ/2 ≤ l) (hl' : ρ/2 ≤ l') (hlU : l ≤ 2*ρ) (hlU' : l' ≤ 2*ρ)
       (hl1 : l ≤ 1) (hl1' : l' ≤ 1) (e : sphere (0:E) 1) :
       |normalized μ.toSphere θ l e-normalized μ.toSphere θ' l' e| ≤
         (2/(lowerConstant μ/2^(Module.finrank ℝ E-1))+
           2*(2^(Module.finrank ℝ E)*upperConstant μ)/(lowerConstant μ/2^(Module.finrank ℝ E-1))^2)*
         (dist θ θ'+2*|l-l'|)/ρ^(Module.finrank ℝ E) := by
   …

   Mentions: OAI.HenonLaneEmden.CapWeights.normalized, OAI.HenonLaneEmden.CapWeights.lowerConstant, OAI.HenonLaneEmden.CapWeights.upperConstant